proposition: Lemma FST_def {A B : Type'} : (@fst A B) = (fun p : prod A B => @ε A (fun x : A => exists y : B, 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 x. exists y. reflexivity. generalize (ε_spec i); fold q; intros [x' h']. inversion h'. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts