∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_4} (f : M → ↥S → M → ↥S → p)
  (H :
    ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
      (AddLocalization.r S) (a, b) (a', b') → (AddLocalization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d')
  (a c : M) (b d : ↥S), (AddLocalization.mk a b).liftOn₂ (AddLocalization.mk c d) f H = f a b c d