| Rank | Theorem | Name |
| 4 | | | Thm*  p:Fmla, rho:Decl, ds,daa:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, a1,a2:Top, tr:trace_env([[daa]] rho). trace_consistent_pred(rho;daa;tr.proj;p)   tc_pred(p;ds;da1;de) closed_pred(p) ([[p]] rho ds da1 de e s a1 tr  [[p]] rho ds da2 de e s a2 tr) | [closed_pred_mng] |
| cites |
| 1 | | | Thm* r:rel(), rho,ds,da1,da2,de,s,e,a1,a2,tr:Top. closed_rel(r) ([[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr) | [closed_rel_mng_sq] |
| 3 | | | Thm* rho:Decl, ds,daa:Collection(dec()), da1:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, tr:trace_env([[daa]] rho), r:rel(). closed_rel(r) tc(r;ds;da1;de) trace_consistent_rel(rho;daa;tr.proj;r) [[r]] rho ds da1 de e s  tr  Prop | [rel_mng_wf_closed] |