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