| Rank | Theorem | Name |
| 2 | | | Thm*  v:vc{i:l}(), ds,da:Collection(dec()), de:sig(), rho:Decl, e:{[[de]] rho}, s:{[[ds]] rho}, tr:trace_env([[da]] rho). tc_vc(v;ds;da;de)   trace_consistent_vc(rho;da;tr.proj;v) vc_mng(v;rho;ds;da;de;e;s;tr)  Prop | [vc_mng_wf] |
| cites |
| 0 | | | Thm* v:Top, rho:Decl. v [[ < > ]] rho | [empty_sts_mng] |
| 0 | | | Thm* p:Fmla, ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, 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) [[p]] rho ds da de e s a tr Prop | [pred_mng_wf] |
| 1 | | | Thm* da:Collection(dec()), rho:Decl, k:Label, w:[[dec_lookup(da;k)]] rho. < k,w > ( [[da]] rho) | [sigma_decls_mng2] |