∀ {ι : Type u_3} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_1} (f : ι → α → β) (x : β)
  (motive : x ∈ Set.range (hs.piecewise f) → Prop) (x_1 : x ∈ Set.range (hs.piecewise f)),
  (∀ (y : α) (hy : hs.piecewise f y = x), motive ⋯) → motive x_1