| Rank | Theorem | Name |
| 2 |
Thm*  ds,da:Collection(dec()), st:Collection(SimpleType), de:sig(), rho:Decl
, e1:{1of([[de]] rho)}, s1,s2:{[[ds]] rho}, a:[[st]] rho, tr:trace_env([[da]] rho), u:Term
, t:SimpleType.
trace_consistent(rho;da;tr.proj;u)  
(x:Label. (x  term_vars(u)) s1.x = s2.x)
t term_types(ds;st;de;u) [[u]] e1 s1 a tr = [[u]] e1 s2 a tr [[t]] rho | [term_mng_equal] |
| cites |
| 0 |
Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType.
s sts v [[s]] rho | [sts_mng_subtype] |
| 0 |
Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x)
, a:SimpleType. mk_dec(x, a) ds y [[a]] rho | [decls_mng_subtype] |
| 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] |