∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] (x x_1 : C)
  (x_2 : x ⟶ x_1) (motive : W.transfiniteCompositionsOfShape J x_2 → Prop)
  (x_3 : W.transfiniteCompositionsOfShape J x_2),
  (∀ (hf : W.TransfiniteCompositionOfShape J x_2), motive ⋯) → motive x_3