proposition: Lemma example: (1 + 0 + 1) * (1 + 1) = (1 + 1) + (1 + 1).
proof: Proof. do_quote. Admitted. End approach_A. Module approach_B. Class Quote (n: nat) := { quote: Expr; eval_quote: n = eval quote }. Arguments quote _ {Quote}. Arguments eval_quote _ {Quote}. Section instances. Context n m `{Quote n} `{Quote m}. Global Program Instance: Quote 0 := { quote := Zero }. Global Program Instance: Quote 1 := { quote := One }. Global Instance: Quote (n + m). Proof. refine {| quote := Plus (quote n) (quote m) |}. simpl. do 2 rewrite <- eval_quote. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Program.Program Coq.Unicode.Utf8