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