fact: Definition eta_path_sigma_uncurried {A} `{P : A -> Type} {u v : sigma P} (p : u = v) : path_sigma_uncurried _ _ (p..1, p..2) = p.
imports: Unicode.Utf8 Coq.Program.Tactics Setoid Relations Equations.Type.All CRelationClasses CMorphisms