∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (s : Set α) (motive : (∃ u ∈ Set.Ioc a b, Set.Ico a u ⊆ s) → Prop)
  (x : ∃ u ∈ Set.Ioc a b, Set.Ico a u ⊆ s),
  (∀ (u : α) (umem : u ∈ Set.Ioc a b) (hu : Set.Ico a u ⊆ s), motive ⋯) → motive x