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* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho}	[decls_mng_monotone]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho}	[decls_mng_record_subtype]
Thm* d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho). d2 d1 u ([[d2]] rho)	[sigma_decls_mng_monotone]
Thm* ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType) , de:sig(), t:Term. ds1 ds2 da1 da2 (a:SimpleType. a term_types(ds1;da1;de;t) a term_types(ds2;da2;de;t))	[term_types_monotone_member]
Thm* ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig() , t:Term. ds1 ds2 da1 da2 term_types(ds1;da1;de;t) term_types(ds2;da2;de;t)	[term_types_monotone]

In prior sections: mb collection mb automata 2

Try larger context: GenAutomata