fact: Definition sum_ind_uncurried {A B} (P : A + B -> Type) (fg : (forall a, P (inl a)) * (forall b, P (inr b))) : forall s, P s := @sum_ind A B P (fst fg) (snd fg).
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall