fact: Definition eq_sig_hprop_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : { a : A | P a }) : u = v <-> (proj1_sig u = proj1_sig v) := conj (fun p => f_equal (@proj1_sig _ _) p) (eq_sig_hprop P_hprop u v).
imports: Notations Ltac Datatypes Logic