is mentioned by

Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType. s sts v [[s]] rho	[sts_mng_subtype]
Thm* c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1)	[member_st_app]
Thm* ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds	[member_dec_lookup]
Thm* s1,s2,s:SimpleType. s st_app1(s1;s2) st_eq(s1;s2s)	[member_st_app1]
Def pred_mentions(p;x) == r:rel(). r p & rel_mentions(r;x)	[pred_mentions]
Def [[sts]] rho == x:{x:SimpleType| x sts }. [[x]] rho	[sts_mng]
Def single_valued_decls(c) == x:Label, t1,t2:SimpleType. mk_dec(x, t1) c mk_dec(x, t2) c t1 = t2	[single_valued_decls]
Def covers_var(A;x) == fr:frame(). fr < fr A.frame | fr.var = x > & (a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > ))	[covers_var]

In prior sections: mb collection

Try larger context: GenAutomata