is mentioned by

Thm* sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho	[sts_mng_functionality]
Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType. s sts v [[s]] rho	[sts_mng_subtype]
Thm* a1,a2,b1,b2:Collection(SimpleType). a1 = a2 b1 = b2 st_app(a1;b1) = st_app(a2;b2)	[st_app_functionality]
Thm* a1,a2,b1,b2:Collection(SimpleType). a1 a2 b1 b2 st_app(a1;b1) st_app(a2;b2)	[st_app_monotone]
Thm* c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1)	[member_st_app]
Thm* x:Label, a1,a2:Collection(dec()). a1 a2 dec_lookup(a1;x) dec_lookup(a2;x)	[dec_lookup_monotone]
Thm* ds1,ds2:Collection(dec()), x:Label. ds1 = ds2 dec_lookup(ds1;x) = dec_lookup(ds2;x)	[dec_lookup_functionality]
Thm* ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds	[member_dec_lookup]
Thm* s1,s2:SimpleType. st_app1(s1;s2) Collection(SimpleType)	[st_app1_wf]
Def VCs{i} == Collection{i'}(vc{i:l}())	[vcs]

In prior sections: mb collection mb automata 1

Try larger context: GenAutomata