| Rank | Theorem | Name |
| 2 | | | Thm*  p1,p2:Fmla, ds1,ds2,daa:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s:{[[ds1]] rho}, a:[[da1]] rho, tr:trace_env([[daa]] rho). trace_consistent_pred(rho;daa;tr.proj;p1)   tc_pred(p1;ds1;da1;de) p1 = p2 ds1 = ds2 da1 = da2 ([[p1]] rho ds1 da1 de e s a tr  [[p2]] rho ds2 da2 de e s a tr) | [pred_mng_functionality] |
| cites |
| 1 | | | Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds1 = ds2 r  {[[ds2]] rho} | [decls_mng_functionality] |
| 0 | | | Thm* r:rel(), ds1,ds2,da:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s:{[[ds1]] rho}, a:[[da1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds1;da1;de) ds1 = ds2 da1 = da2 ([[r]] rho ds1 da1 de e s a tr [[r]] rho ds2 da2 de e s a tr) | [rel_mng_functionality] |
| 0 | | | Thm* sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho | [sts_mng_functionality] |
| 0 | | | Thm* r:rel(), ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). ds1 = ds2 da1 = da2 (tc(r;ds1;da1;de) tc(r;ds2;da2;de)) | [tc_functionality] |