∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} [inst_1 : PredOrder α]
  (motive : (x : ↑s) → (x ≤ if h : Order.pred ↑x ∈ s then ⟨Order.pred ↑x, h⟩ else x) → Prop) (x : ↑s)
  (h : x ≤ if h : Order.pred ↑x ∈ s then ⟨Order.pred ↑x, h⟩ else x),
  (∀ (x : α) (hx : x ∈ s) (h : ⟨x, hx⟩ ≤ if h : Order.pred ↑⟨x, hx⟩ ∈ s then ⟨Order.pred ↑⟨x, hx⟩, h⟩ else ⟨x, hx⟩),
      motive ⟨x, hx⟩ h) →
    motive x h