proposition: Lemma quote_equality `{v: Vars V} `{v': Vars V'} (l r: M) `{!Quote novars l v} `{!Quote v r v'}: let heap := (merge v v') in eval _ heap (ua.map_var msig (obvious: False + V → V + V') quote) = eval _ heap quote → l = r.
proof: Proof. Proof with intuition. intros heap. destruct Quote0, Quote1. subst. subst heap. simpl. intro. rewrite <- H0. rewrite ua.eval_map_var. cut (eval _ (merge novars v) quote0 ≡ ua.eval msig (λ _, merge v v' ∘ obvious) quote0). intro E. simpl in *. rewrite E. reflexivity. apply (@ua.eval_strong_proper msig (λ _, M) _ _ (ne_list.one tt))... repeat intro... Qed.
imports: MathClasses.interfaces.abstract_algebra