Nuprl - mb_automata_3 LEMMAs for tc_closed

Rank	Theorem	Name
2	Thm* r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_rel(r) tc(r;ds;da1;de) tc(r;ds;da2;de)	[tc_closed_rel]
cites
0	Thm* r:rel(), i:. closed_rel(r) i < \|\|r.args\|\| closed_term(r.args[i])	[closed_rel_args]
1	Thm* t:Term, ds:Collection(dec()), da1,da2:Collection(SimpleType) , de:sig(). closed_term(t) term_types(ds;da1;de;t) = term_types(ds;da2;de;t)	[term_types_closed]