| Rank | Theorem | Name |
| 2 |
Thm*  ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl
, t:Term, s,s':{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[da]] rho
, tr:trace_env([[daa]] rho).
trace_consistent(rho;daa;tr.proj;t)   a  term_types(ds;da;de;t) [[t]] e s s' v tr [[a]] rho | [term_typing2] |
| cites |
| 0 |
Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType.
s sts v [[s]] rho | [sts_mng_subtype] |
| 1 |
Thm* ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label
, t:SimpleType. t dec_lookup(ds;x) s.x [[t]] rho | [record_select_wf_decls_mng2] |
| 1 |
Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label.
trace_consistent(rho;da;tr.proj;trace(y1)) tr.y1 [[lbl_pr( < Trace, y1 > )]] rho | [tproj_w_f2] |