t:Term, as:(Label
Term) List.
(x:Label. unprime(apply_alist(as;x;x)) = x) 
unprime(term_subst(as;t)) = unprime(t)x:T, l:T List. (y:T. Dec(x = y)) Dec((x 
l))| Theorem | Name |
|
Thm* t:Term, as:(LabelTerm) List.
(x:Label. unprime(apply_alist(as;x;x)) = x) unprime(term_subst(as;t)) = unprime(t) | [trivial_term_subst] |
| cites | |
|
Thm* x:T, l:T List. (y:T. Dec(x = y)) Dec((x l)) | [l_member_decidable] |