fact: Definition eq_sig2_hprop {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q) (u v : { a : A | P a & Q a }) (p : u = v :> { a : A | P a }) : u = v := eq_sig2 u v (proj1_sig_eq p) (proj2_sig_eq p) (Q_hprop _ _ _).
imports: Notations Ltac Datatypes Logic