∀ {α : Type u_2} {β : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β}
  (x x_1 : α) (x_2 : β) (motive : x_2 ∈ Set.Ioc (f x) (f (Order.succ x)) ⊓ Set.Ioc (f x_1) (f (Order.succ x_1)) → Prop)
  (x_3 : x_2 ∈ Set.Ioc (f x) (f (Order.succ x)) ⊓ Set.Ioc (f x_1) (f (Order.succ x_1))),
  (∀ (left : f x < x_2) (h₁ : x_2 ≤ f (Order.succ x)) (h₂ : f x_1 < x_2) (right : x_2 ≤ f (Order.succ x_1)), motive ⋯) →
    motive x_3