fact: Definition path_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : @sigT A P) : u = v <-> (projT1 u = projT1 v) := conj (f_equal projT1) (path_sigT_hprop P_hprop u v).
imports: Fiat.Common.Equality