Nuprl - mb_automata_3 LEMMAs for term_subst_mentions

Rank	Theorem	Name
2	Thm* as:(LabelTerm) List, g:Label, t:Term. subst_mentions_trace(as) term_mentions_guard(g;term_subst(as;t)) term_mentions_guard(g;t)	[term_subst_mentions_guard]
cites
0	Thm* g:Label, t:Term. term_mentions_guard(g;t) mentions_trace(t)	[mentions_guard_mentions_trace]
1	Thm* as:(LabelT) List, d:T, x:Label. (apply_alist(as;x;d) 2of(unzip(as))) apply_alist(as;x;d) = d	[apply_alist_property]