∀ {α : Type u_1} {s : Set α} [inst : PseudoMetricSpace α] (c : α) (motive : (∃ r, s ⊆ Metric.ball c r) → Prop)
  (x : ∃ r, s ⊆ Metric.ball c r), (∀ (_r : ℝ) (hr : s ⊆ Metric.ball c _r), motive ⋯) → motive x