Nuprl - mb automata 2 LEMMAs for rel subst2 addprime

Rank	Theorem	Name
4			Thm* r:rel(), as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) rel_subst2(as;(r)') = rel_subst(as;r)	[rel_subst2_addprime]
cites
0			Thm* as:A List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)	[map_map_sq]
0			Thm* a,b:T List. \|\|a\|\| = \|\|b\|\| (i:. i < \|\|a\|\| a[i] = b[i]) a = b	[list_extensionality]
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]