{J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        {d : F.WellOrderInductionData} →
          [inst_2 : OrderBot J] →
            {val₀ : F.obj (Opposite.op ⊥)} →
              {j : J} →
                (val : F.obj (Opposite.op j)) →
                  F.map (CategoryTheory.homOfLE ⋯).op val = val₀ →
                    (∀ (i : J) (hi : i < j),
                        F.map (CategoryTheory.homOfLE ⋯).op val =
                          d.succ i ⋯ (F.map (CategoryTheory.homOfLE ⋯).op val)) →
                      (∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
                          F.map (CategoryTheory.homOfLE hij).op val =
                            d.lift i hi
                              ⟨fun x =>
                                match x with
                                | Opposite.op ⟨k, hk⟩ => F.map (CategoryTheory.homOfLE ⋯).op val,
                                ⋯⟩) →
                        d.Extension val₀ j