| Rank | Theorem | Name |
| 2 | | | 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] |
| cites |
| 0 | | | Thm* da:Collection(dec()), P:Fmla, rho:Decl, te:(Label  Label ). trace_consistent_pred(rho;da;te;P) trace_consistent_pred(rho;da;te;pred_unprime(P)) | [trace_consistent_pred_unprime] |
| 0 | | | 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] |
| 1 | | | Thm* r:rel(), rho,ds,da,de,e,s,s',a,tr:Top. rel_mng_2(rel_unprime(r); rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s a tr | [rel_mng_2_unprime] |