{V:Type0} {v: Vars V} {V':Type0} {v': Vars V'} (l r: R) `{!Quote noVars l v} `{!Quote v r v'} : let heap := (merge v v') in eval heap (expr_map sum_forget (quote l)) = eval heap (quote r) -> l = r. Proof. intros ? E. rewrite <-(eval_quote l),<-(eval_quote r). path_via (eval heap (expr_map sum_forget (quote l))). rewrite eval_map. apply eval_ext. intros [[]|?]. reflexivity. Qed.
Require Import