At: term typing
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
By:
UnivCD
THEN
Unfold `member` 0
THEN
BackThruLemma'
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
Generated subgoals:None
About: