fact: Definition sig_coind_uncurried `{A : X -> Type} (P : forall x, A x -> Type) : { f : forall x, A x & forall x, P x (f x) } -> (forall x, sig (P x)) := fun fg => fun x => (fg.1 x ; fg.2 x).
imports: HoTT.Basics Types.Arrow Types.Paths