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* A:ioa{i:l}(), I:Fmla. ioa_trans_all{i}(A;I) VCs	[ioa_trans_all_wf]
Thm* vs:VCs{i}, ds,da:Collection{i}(dec()), de:sig(). tc_vcs{i}(vs;ds;da;de) Prop{i'}	[tc_vcs_wf]

Try larger context: GenAutomata