∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} (_x : α) (motive : (∃ c ∈ s, c < _x) → Prop)
  (x : ∃ c ∈ s, c < _x), (∀ (_y : α) (ys : _y ∈ s) (hy : _y < _x), motive ⋯) → motive x