{M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {p : AddLocalization S → Sort u} →
        (f : (a : M) → (b : ↥S) → p (AddLocalization.mk a b)) →
          (∀ {a c : M} {b d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) →
            (x : AddLocalization S) → p x