∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  [inst_2 : WellFoundedLT α] (isMin isMin_1 : (a : α) → IsMin a → motive a),
  isMin = isMin_1 →
    ∀ (succ succ_1 : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)),
      succ = succ_1 →
        ∀ (isSuccLimit isSuccLimit_1 : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a),
          isSuccLimit = isSuccLimit_1 →
            SuccOrder.limitRecOn b isMin succ isSuccLimit = SuccOrder.limitRecOn b isMin_1 succ_1 isSuccLimit_1