is mentioned by

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]
Def [[rn]] rho e == Case(rn) Case eq(Q) = > x,y. x = y [[Q]] rho Case R = > e.R Default = > True	[relname_mng]
Def [[d]] rho == Case(d) Case x : s = > x:[[s]] rho	[dec_mng]
Def [[l]] rho == reduce(s,m. [[s]] rhom;Prop;l)	[st_list_mng]
Def [[sts]] rho == x:{x:SimpleType| x sts }. [[x]] rho	[sts_mng]

Try larger context: GenAutomata