∀ {α : Type u_1} [inst : Preorder α] (b : α) (motive : (c : WithTop α) → ↑b < c → Prop) (c : WithTop α) (hbc : ↑b < c),
  (∀ (hbc : ↑b < ⊤), motive none hbc) → (∀ (c : α) (hbc : ↑b < ↑c), motive (some c) hbc) → motive c hbc