fact: Definition upd (A:Type): (ExVar A) -> A -> Env -> Env := fun x => match x in (ExVar A) return A -> Env -> Env with | VX => fun vx e => (vx,snd e) | VY => fun vy e => (fst e,vy) end.
imports: ZArith Znumtheory hoarelogic Zwf Wellfounded Lia