∀ {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.strictLimitsOfShape J a → Prop},
  (∀ (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] (hF : ∀ (j : J), P (F.obj j)),
      motive (CategoryTheory.Limits.limit F) ⋯) →
    ∀ {a : C} (t : P.strictLimitsOfShape J a), motive a t