Nuprl - mb automata 4 LEMMAs for trace consistent rel subst2

Rank	Theorem	Name
3			Thm* r:rel(), as:(LabelTerm) List, daa:Collection(dec()), rho:Decl, te:(LabelLabel). trace_consistent_rel(rho;daa;te;r) subst_mentions_trace(as) trace_consistent_rel(rho;daa;te;rel_subst2(as;r))	[trace_consistent_rel_subst2]
cites
2			Thm* as:(LabelTerm) List, g:Label, t:Term. subst_mentions_trace(as) term_mentions_guard(g;term_subst2(as;t)) term_mentions_guard(g;t)	[term_subst2_mentions_guard]