∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.limitsOfShape J x → Prop},
  (∀ (X₁ X₂ : CategoryTheory.Functor J C) (c₁ : CategoryTheory.Limits.Cone X₁) (c₂ : CategoryTheory.Limits.Cone X₂)
      (x : CategoryTheory.Limits.IsLimit c₁) (h₂ : CategoryTheory.Limits.IsLimit c₂) (f : X₁ ⟶ X₂)
      (x_1 : W.functorCategory J f),
      motive (h₂.lift { pt := c₁.pt, π := CategoryTheory.CategoryStruct.comp c₁.π f }) ⋯) →
    ∀ ⦃X Y : C⦄ {x : X ⟶ Y} (t : W.limitsOfShape J x), motive x t