is mentioned by

Thm* A:ioa{i:l}(), I:Fmla, rho:Decl, te:(LabelLabel). ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;I) (vVCs(A;I).trace_consistent_vc(rho;A.da;te;v))	[trace_consistent_ioa_inv_vc]
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* p:Collection(rel()), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc_pred(p;ds;da;de) (rp.tc(r;ds;da;de))	[tc_pred_col_all]
Def trace_consistent_pred(rho;da;R;p) == (rp.trace_consistent_rel(rho;da;R;r))	[trace_consistent_pred]

In prior sections: mb collection

Try larger context: GenAutomata