is mentioned by

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]
Thm* d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho). d1 = d2 u ([[d2]] rho)	[sigma_decls_mng_functionality]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:([[ds1]] rho). ds1 = ds2 r ([[ds2]] rho)	[decls_mng_functionality_sigma]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds1 = ds2 r {[[ds2]] rho}	[decls_mng_functionality]
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]
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_functionality]

In prior sections: mb collection mb automata 2

Try larger context: GenAutomata