is mentioned by

Thm* sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho	[sts_mng_functionality]
Thm* t:SimpleType, rho:Decl, v:[[t]] rho. v [[ < t > ]] rho	[sts_mng_singleton]
Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType. s sts v [[s]] rho	[sts_mng_subtype]
Thm* v:Top, rho:Decl. v [[ < > ]] rho	[empty_sts_mng]

Try larger context: GenAutomata