proposition: Lemma NUMFST_NUMPAIR x y : NUMFST (NUMPAIR x y) = x.
proof: Proof. unfold NUMFST. generalize (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))), (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0))))))), (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))), (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0))))))), (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0))))))), NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))). generalize (prod nat (prod nat (prod nat (prod nat (prod nat nat))))); intros A a. match goal with |- ε ?x _ _ = _ => set (Q := x); set (fst := ε Q) end. assert (i: exists x, Q x). exists (fun _ => NUMFST0). unfold Q. intros _. exists NUMSND0. intros x' y'. rewrite NUMFST0_NUMPAIR, NUMSND0_NUMPAIR. auto. generalize (ε_spec i). change (Q fst -> fst a (NUMPAIR x y) = x). intro h. destruct (h a) as [snd j]. destruct (j x y) as [j1 j2]. exact j1. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat