proposition: Lemma quote_equality {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: 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.
imports: HoTT.Classes.interfaces.abstract_algebra