∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderFiniteCoproducts] {J : Type u_2} [Finite J] {f : J → C} {F : CategoryTheory.Limits.Cofan f}
  (hF : CategoryTheory.Limits.IsColimit F), (∀ (j : J), P (f j)) → P F.pt