Term) List6.
v:Label. (v 
[x2]) 
(v 1of(unzip(as)))
apply_alist(as;x2;x2') = apply_alist(as;x2;x2)
Type{i'}
as:(LabelTerm) List.
(v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)
as:(LabelTerm) List. (v:Label. (v [x2]) (v 1of(unzip(as)))) apply_alist(as;x2;x2') = apply_alist(as;x2;x2)
| 1 | 5. as: (LabelTerm) List 6. v:Label. (v [x2]) (v 1of(unzip(as))) apply_alist(as;x2;x2') = apply_alist(as;x2;x2) |
About:
 |  |  |  |  |  |
 |  |  |  |  |