proposition: Lemma NUMSND_NUMPAIR x y : NUMSND (NUMPAIR x y) = y.
proof: Proof. unfold NUMSND. 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 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0))))))), (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))), NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (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 (snd := ε Q) end. assert (i: exists x, Q x). exists (fun _ => NUMSND1). unfold Q. intros _. intros x' y'. rewrite NUMFST_NUMPAIR, NUMSND1_NUMPAIR. auto. generalize (ε_spec i). change (Q snd -> snd a (NUMPAIR x y) = y). intro h. destruct (h a x y) as [h1 h2]. exact h2. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat