proposition: Lemma ex1_def : forall {A : Type'}, (@ex1 A) = (fun P : A -> Prop => (ex P) /\ (forall x : A, forall y : A, ((P x) /\ (P y)) -> x = y)).
proof: Proof. intro A. unfold ex1. apply fun_ext; intro P. unfold unique. apply prop_ext. intros [x [px u]]. split. apply (ex_intro P x px). intros a b [ha hb]. transitivity x. symmetry. apply u. exact ha. apply u. exact hb. intros [[x px] u]. apply (ex_intro _ x). split. exact px. intros y py. apply u. split. exact px. exact py. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts