proposition: Lemma le_def : le = (@ε (arr (prod nat nat) (arr nat (arr nat Prop'))) (fun le' : (prod nat nat) -> nat -> nat -> Prop => forall _2241 : prod nat nat, (forall m : nat, (le' _2241 m ( 0)) = (m = ( 0))) /\ (forall m : nat, forall n : nat, (le' _2241 m (S n)) = ((m = (S n)) \/ (le' _2241 m n)))) (@pair nat nat ( (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 (BIT1 0))))))) ( (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 (BIT1 0))))))))).
proof: Proof. generalize (@pair nat nat ( (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 (BIT1 0))))))) ( (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 (BIT1 0)))))))); generalize (prod nat nat); intros A a. match goal with [|- _ = ε ?x _] => set (Q := x) end. assert (i : exists q, Q q). exists (fun _ => le). split; simpl; intro x. apply prop_ext; intro h. symmetry. apply Arith_base.le_n_0_eq_stt. exact h. rewrite h. reflexivity. intro n. apply prop_ext; lia. generalize (ε_spec i a). intros [h0 hs]. apply fun_ext; intro x. apply fun_ext; intro y. apply prop_ext. induction 1. induction x. rewrite h0. reflexivity. rewrite hs. left. reflexivity. rewrite hs. right. assumption. induction y. rewrite h0. intro h. rewrite h. reflexivity. rewrite hs. intros [h|h]. rewrite h. reflexivity. apply le_S. apply IHy. exact h. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat