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