∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (self self_1 : F.WellOrderInductionData),
  self = self_1 →
    ∀ (j : J) (hj : ¬IsMax j) (x x_1 : F.obj (Opposite.op j)), x = x_1 → self.succ j hj x = self_1.succ j hj x_1