| Rank | Theorem | Name |
| 4 | | | Thm*  A:ioa{i:l}(), de:sig(), rho:Decl, e:{[[de]] rho}. tc_ioa(A;de)    ioa_mentions_trace(A) [[A]] rho de e  sm{i:l}() | [ioa_mng_wf] |
| cites |
| 1 | | | Thm* ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label, t:SimpleType. mk_dec(x, t) ds s.x [[t]] rho | [record_select_wf_decls_mng] |
| 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] |
| 0 | | Thm* da,ds:Decl, init:({ds}  Prop), trans:({ds}( da){ds}Prop). mk_sm(da, ds, init, trans) sm{i:l}() | [mk_sm_wf] |
| 1 | | | Thm* rho:Decl, r:rel(), da:Collection(dec()), R:(LabelLabel ). rel_mentions_trace(r) trace_consistent_rel(rho;da;R;r) | [no_mention_implies_consistent_rel] |
| 3 | | | Thm* ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, t:Term, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent(rho;da;tr.proj;t) a term_types(ds;st1;de;t) [[t]] e s v tr [[a]] rho | [term_typing] |
| 0 | | | Thm* t:SimpleType, rho:Decl, v:[[t]] rho. v [[ < t > ]] rho | [sts_mng_singleton] |
| 0 | | | Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType. s sts v [[s]] rho | [sts_mng_subtype] |
| 0 | | | Thm* rho:Decl, t:Term, da:Collection(dec()), R:(LabelLabel). mentions_trace(t) trace_consistent(rho;da;R;t) | [no_mention_implies_consistent_term] |