is mentioned by

Thm* r:rel(), de:sig(), ds1,ds2:Collection(dec()) , da1,da2:Collection(SimpleType). ds1 ds2 da1 da2 tc(r;ds1;da1;de) tc(r;ds2;da2;de)	[tc_monotone]
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* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc(rel_unprime(r);ds;da;de)	[tc_unprime]
Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc((r)';ds;da;de)	[tc_addprime]
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]
Thm* r:rel(), ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType) , de:sig(). ds1 = ds2 da1 = da2 (tc(r;ds1;da1;de) tc(r;ds2;da2;de))	[tc_functionality]

Try larger context: GenAutomata