∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : WellFoundedLT α]
  (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a) [inst_3 : NoMaxOrder α]
  (b : α),
  SuccOrder.prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b ⋯ (SuccOrder.prelimitRecOn b succ isSuccPrelimit)