is mentioned by

Thm* sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho	[sts_mng_functionality]
Thm* a1,a2,b1,b2:Collection(SimpleType). a1 = a2 b1 = b2 st_app(a1;b1) = st_app(a2;b2)	[st_app_functionality]
Thm* ds1,ds2:Collection(dec()), x:Label. ds1 = ds2 dec_lookup(ds1;x) = dec_lookup(ds2;x)	[dec_lookup_functionality]

In prior sections: mb collection

Try larger context: GenAutomata