is mentioned by

Thm* vs:VCs{i}, ds,da:Collection{i}(dec()), de:sig(), rho:Decl{i}, e:{sig_mng{i:l}(de; rho)}, s:{[[ds]] rho}, tr:trace_env([[da]] rho). tc_vcs{i}(vs;ds;da;de) (vvs.trace_consistent_vc(rho;da;tr.proj;v)) [[vs]] rho ds da de e s tr Prop{i'}	[vcs_mng_wf]
Thm* vs:VCs{i}, ds,da:Collection{i}(dec()), de:sig(). tc_vcs{i}(vs;ds;da;de) Prop{i'}	[tc_vcs_wf]
Thm* v:vc{i:l}(), ds,da:Collection(dec()), de:sig(), rho:Decl, e:{[[de]] rho}, s:{[[ds]] rho}, tr:trace_env([[da]] rho). tc_vc(v;ds;da;de) trace_consistent_vc(rho;da;tr.proj;v) vc_mng(v;rho;ds;da;de;e;s;tr) Prop	[vc_mng_wf]
Thm* v:vc{i:l}(), ds,da:Collection(dec()), de:sig(). tc_vc(v;ds;da;de) Prop	[tc_vc_wf]
Thm* p:Fmla, ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s,s':{[[ds]] rho}, tr:trace_env([[daa]] rho). trace_consistent_pred(rho;daa;tr.proj;p) tc_pred(p;ds;da;de) closed_pred(p) pred_mng_2(p; rho; ds; da; de; e; s; s'; ; tr) Prop	[pred_mng_2_wf_closed]
Thm* p:Fmla, ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s:{[[ds]] rho}, a:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent_pred(rho;daa;tr.proj;p) tc_pred(p;ds;da;de) [[p]] rho ds da de e s a tr Prop	[pred_mng_wf]
Thm* p:Fmla, ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s,s':{[[ds]] rho}, a:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent_pred(rho;daa;tr.proj;p) tc_pred(p;ds;da;de) pred_mng_2(p; rho; ds; da; de; e; s; s'; a; tr) Prop	[pred_mng_2_wf]
Thm* p:Fmla, rho:Decl, da:Collection(dec()), R:(LabelLabel). trace_consistent_pred(rho;da;R;p) Prop	[trace_consistent_pred_wf]
Thm* rho:Decl, ds,daa:Collection(dec()), da1:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, tr:trace_env([[daa]] rho), r:rel(). closed_rel(r) tc(r;ds;da1;de) trace_consistent_rel(rho;daa;tr.proj;r) [[r]] rho ds da1 de e s tr Prop	[rel_mng_wf_closed]
Thm* r:rel(), ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType), e:{[[de]] rho}, s:{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds;st1;de) [[r]] rho ds st1 de e s a tr Prop	[rel_mng_wf]
Thm* r:rel(), ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType), e:{[[de]] rho}, s,s':{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds;st1;de) rel_mng_2(r; rho; ds; st1; de; e; s; s'; a; tr) Prop	[rel_mng_2_wf]

In prior sections: core well fnd int 1 bool 1 fun 1 int 2 list 1 rel 1 mb basic mb nat mb list 1 mb collection mb list 2 mb automata 1 mb automata 2 mb state machine mb automata 3

Try larger context: GenAutomata