| 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] |
| 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] |