1of(unzip(as)))
unprime(apply_alist(as;x;x')) = unprime(x')
(x 1of(unzip(as))) unprime(apply_alist(as;x;x')) = unprime(x')
Type{i'}
as:(Label
Term) List.
(x:Label. unprime(apply_alist(as;x;x)) = x) 
unprime(term_subst(as;t)) = unprime(t)Term) Listx:Label. unprime(apply_alist(as;x;x)) = x 1of(unzip(as))) 
(x 1of(unzip(as))) unprime(apply_alist(as;x;x')) = unprime(x')| 1 | 8. (x 1of(unzip(as))) unprime(apply_alist(as;x;x')) = unprime(x') |
| 2 | 8. (x 1of(unzip(as))) unprime(apply_alist(as;x;x')) = unprime(x') |
About:
 |  |  |  |  |  |  |  |  |  |