{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {motive : W.IsStableUnderTransfiniteComposition → Sort u_1} →
        (t : W.IsStableUnderTransfiniteComposition) →
          ((isStableUnderTransfiniteCompositionOfShape :
                ∀ (J : Type w) [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
                  [inst_4 : WellFoundedLT J], W.IsStableUnderTransfiniteCompositionOfShape J) →
              motive ⋯) →
            motive t