∀ {K : Type u_1} [hK : NormedField K] (U : Set K) (motive : (∃ ε > 0, Metric.ball 0 ε ⊆ U) → Prop)
  (x : ∃ ε > 0, Metric.ball 0 ε ⊆ U), (∀ (ε : ℝ) (hε : ε > 0) (h : Metric.ball 0 ε ⊆ U), motive ⋯) → motive x