proposition: Lemma add_def : Nat.add = (@ε (arr nat (arr nat (arr nat nat'))) (fun add' : nat -> nat -> nat -> nat => forall _2155 : nat, (forall n : nat, (add' _2155 ( 0) n) = n) /\ (forall m : nat, forall n : nat, (add' _2155 (S m) n) = (S (add' _2155 m n)))) ( (BIT1 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))).
proof: Proof. generalize ( (BIT1 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0))))))). intro a. match goal with [|- _ = ε ?x _] => set (Q := x) end. assert (i : exists q, Q q). exists (fun _ => Nat.add). split; reflexivity. generalize (ε_spec i a). intros [h0 hs]. apply fun_ext; intro x. apply fun_ext; intro y. induction x; simpl. rewrite h0. reflexivity. rewrite hs, IHx. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat