{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : WellFoundedLT J] →
                {X Y : C} →
                  {f : X ⟶ Y} →
                    {motive : W.TransfiniteCompositionOfShape J f → Sort u_1} →
                      ((toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f) →
                          (map_mem :
                              ∀ (j : J),
                                ¬IsMax j → W (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯))) →
                            motive
                              { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape,
                                map_mem := map_mem }) →
                        (t : W.TransfiniteCompositionOfShape J f) → motive t