fact: Definition eq_ex_hprop_iff {A : Prop} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : exists a : A, P a) : u = v <-> (ex_proj1 u = ex_proj1 v) := conj (fun p => f_equal (@ex_proj1 _ _) p) (eq_ex_hprop P_hprop u v).
imports: Notations Ltac