proposition: Lemma quote_equality {V} {v: Vars V} {V'} {v': Vars V'} (l r: Value) `{!Quote novars l v} `{!Quote v r v'}: let heap := (merge v v') in eval heap (map_var monkey quote) = eval heap quote → l = r.
proof: Proof. Proof with intuition. destruct Quote0 as [lq []]. destruct Quote1 as [rq []]. intros heap H. subst heap. simpl in H. rewrite <- H, eval_map_var. apply eval_proper... intro... Qed.
imports: Coq.Classes.Morphisms Coq.Program.Program Coq.Unicode.Utf8