fact: Definition path_sig {A : Type} {P : A -> Prop} (u v : sig P) (p : proj1_sig u = proj1_sig v) (q : eq_rect _ _ (proj2_sig u) _ p = proj2_sig v) : u = v := path_sig_uncurried u v (exist _ p q).
imports: Fiat.Common.Equality