∀ {K : Type u_1} [hK : NormedField K] [inst : IsUltrametricDist K] (U : Set K)
  (motive : (∃ γ, {x | NormedField.valuation x < ↑γ} ⊆ U) → Prop) (x : ∃ γ, {x | NormedField.valuation x < ↑γ} ⊆ U),
  (∀ (ε : NNRealˣ) (hε : {x | NormedField.valuation x < ↑ε} ⊆ U), motive ⋯) → motive x