∀ {X : Type u_1} [inst : UniformSpace X] (x : X) (K : Set X)
  (motive : (∃ V ∈ uniformity X, IsOpen V ∧ UniformSpace.ball x V ⊆ Kᶜ) → Prop)
  (x_1 : ∃ V ∈ uniformity X, IsOpen V ∧ UniformSpace.ball x V ⊆ Kᶜ),
  (∀ (O : Set (X × X)) (hOu : O ∈ uniformity X) (hOo : IsOpen O) (hbO : UniformSpace.ball x O ⊆ Kᶜ), motive ⋯) →
    motive x_1