Nuprl - mb_automata_3 LEMMAs for trivial_rel

Rank	Theorem	Name
2	Thm* r:rel(), as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) rel_unprime(rel_subst(as;r)) = rel_unprime(r)	[trivial_rel_subst]
cites
0	Thm* a,b:T List. \|\|a\|\| = \|\|b\|\| (i:. i < \|\|a\|\| a[i] = b[i]) a = b	[list_extensionality]
1	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]