{J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        {motive : F.WellOrderInductionData → Sort u_1} →
          (t : F.WellOrderInductionData) →
            ((succ : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j))) →
                (map_succ :
                    ∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)),
                      F.map (CategoryTheory.homOfLE ⋯).op (succ j hj x) = x) →
                  (lift : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j)) →
                    (map_lift :
                        ∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j),
                          F.map (CategoryTheory.homOfLE ⋯).op (lift j hj x) = ↑x (Opposite.op ⟨i, hi⟩)) →
                      motive { succ := succ, map_succ := map_succ, lift := lift, map_lift := map_lift }) →
              motive t