is mentioned by

Thm* rho:Decl, d:dec(). [[d]] rho Decl	[dec_mng_wf]
Thm* l:SimpleType List, rho:Decl{i}. [[l]] rho{i} Type{i'}	[st_list_mng_wf]
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]
Thm* u:Term, d:Decl, tr:trace_env(d), a:(d), e,s,v:Top. affects_trace(tr.proj;kind(a);u) ([[u]] e s v tappend(tr;a) ~ [[u]] e s v tr)	[term_mng_tappend]

In prior sections: mb declaration mb record mb events mb automata 1

Try larger context: GenAutomata