∀ {α : Type u_2} {ι : Type u_1} [inst : LinearOrder α] {s : Finset ι} {f : ι → α} {a : α}
  (motive : (∃ b ∈ s, a < f b) → Prop) (x : ∃ b ∈ s, a < f b),
  (∀ (b : ι) (hb : b ∈ s) (hlt : a < f b), motive ⋯) → motive x