x:Term, as:(Label
Term) List. (v:Label. (v 
term_vars(x)) 
(v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)l1,l2:Label. l1 =
l2 
l1 = l2| Rank | Theorem | Name | ||
| 3 | Thm* x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x) | [term_subst2_addprime] | ||
| cites | ||||
| 2 | Thm* l1,l2:Label. l1 = l2 l1 = l2 | [eq_lbl_iff] |