∀ {K : Type u_1} [inst : Field K] {A : ValuationSubring K} {a : K}
  (motive : (∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥A) → Prop)
  (x : ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥A),
  (∀ (w : a ∈ A) (h : ⟨a, w⟩ ∈ IsLocalRing.maximalIdeal ↥A), motive ⋯) → motive x