proposition: Lemma SND_def {A B : Type'} : (@snd A B) = (fun p : prod A B => @ε B (fun y : B => exists x : A, p = (@pair A B x y))).
proof: Proof. apply fun_ext; intros [x y]. simpl. match goal with [|- _ = ε ?x] => set (Q := x); set (q := ε Q) end. assert (i : exists x, Q x). exists y. exists x. reflexivity. generalize (ε_spec i); fold q; intros [x' h]. inversion h. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts