is mentioned by

Thm* r:rel(), as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) (x:Label. (x rel_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) tc(rel_subst(as;r);ds;da;de)	[rel_subst_tc]
Thm* r:rel(), as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) (x:Label. (x rel_primed_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) tc(rel_subst2(as;r);ds;da;de)	[rel_subst2_tc]
Thm* ds:Collection(dec()), rho:Decl, a:([[ds]] rho), x:Label. mk_dec(kind(a), x) ds value(a) rho(x)	[sigma_decls_mng_value2]
Thm* ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label , t:SimpleType. mk_dec(x, t) ds s.x [[t]] rho	[record_select_wf_decls_mng]
Thm* ds1,ds2:Collection(dec()), x,y:Label, rho:Decl , v:[[ds1]] rho(x). (d:dec(). d ds2 d.lbl = y mk_dec(x, d.typ) ds1) v [[ds2]] rho(y)	[decls_mng_rename_member]
Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x) , a:SimpleType. mk_dec(x, a) ds y [[a]] rho	[decls_mng_subtype]
Thm* t:Term, s:SimpleType, as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(SimpleType), de:sig(). s term_types(ds;da;de;t) (x:Label. (x term_primed_vars(t)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) s term_types(ds;da;de;term_subst2(as;t))	[term_subst2_tc]
Thm* t:Term, s:SimpleType, as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(SimpleType), de:sig(). s term_types(ds;da;de;t) (x:Label. (x term_vars(t)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) s term_types(ds;da;de;term_subst(as;t))	[term_subst_tc]
Def tc_smt(s;ds;da;de) == mk_dec(s.lbl, s.typ) ds & s.typ term_types(ds;da;de;s.term)	[tc_smt]

In prior sections: mb automata 2

Try larger context: GenAutomata