apply_alist(as;x;x') = apply_alist(as;x;x) 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))) unprime(apply_alist(as;x;x')) = unprime(x')| 1 | apply_alist(as;x;x') = apply_alist(as;x;x) |
| 2 | unprime(apply_alist(as;x;x)) = unprime(x') |
About:
 |  |  |  |  |  |  |  |  |