∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {motive : (a : C) → P.strictColimitsOfShape J a → Prop} {a : C}
  (t : P.strictColimitsOfShape J a),
  (∀ (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] (hF : ∀ (j : J), P (F.obj j)),
      motive (CategoryTheory.Limits.colimit F) ⋯) →
    motive a t