proposition: Lemma do_quote {n m} `{Quote n} `{Quote m}: eval (quote n) = eval (quote m) → n = m.
proof: Proof. intros. rewrite (eval_quote n), (eval_quote m). assumption. Qed.
imports: Coq.Classes.Morphisms Coq.Program.Program Coq.Unicode.Utf8