fact: Definition eq_ex2_hprop {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) (p : u = v :> exists a : A, P a) : u = v := eq_ex2 u v (ex_proj1_eq p) (ex_proj2_eq p) (Q_hprop _ _ _).
imports: Notations Ltac