proposition: Lemma ex_def : forall {A : Type'}, (@ex A) = (fun P : A -> Prop => forall q : Prop, (forall x : A, (P x) -> q) -> q).
proof: Proof. intro A. apply fun_ext; intro p. apply prop_ext. intros [x px] q pq. eapply pq. apply px. intro h. apply h. intros x px. apply (ex_intro p x px). Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts