fact: Definition path_sigT {A : Type} {P : A -> Type} (u v : sigT P) (p : projT1 u = projT1 v) (q : eq_rect _ _ (projT2 u) _ p = projT2 v) : u = v := path_sigT_uncurried u v (existT _ p q).
imports: Fiat.Common.Equality