fact: Definition eq_ex2_hprop_iff {A : Prop} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q) (u v : exists2 a : A, P a & Q a) : u = v <-> (u = v :> exists a : A, P a) := conj (fun p => f_equal (@ex_of_ex2 _ _ _) p) (eq_ex2_hprop Q_hprop u v).
imports: Notations Ltac