∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (z : N) (motive : (∃ x, z * f ↑x.2 = f x.1) → Prop) (x : ∃ x, z * f ↑x.2 = f x.1),
  (∀ (a : M × ↥S) (ha : z * f ↑a.2 = f a.1), motive ⋯) → motive x