is mentioned by

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(pred_unprime(p); rho; ds; da; de; e; s; s'; a; tr) [[p]] rho ds da de e s a tr)	[pred_mng2_unprime]
Thm* da:Collection(dec()), P:Fmla, rho:Decl, te:(LabelLabel). trace_consistent_pred(rho;da;te;P) trace_consistent_pred(rho;da;te;pred_unprime(P))	[trace_consistent_pred_unprime]
Thm* P:Fmla, ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc_pred(P;ds;da;de) tc_pred(pred_unprime(P);ds;da;de)	[tc_pred_unprime]

Try larger context: GenAutomata