∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {p : Type u_4} (f : M → ↥S → p)
  (H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d), Localization.liftOn 0 f H = f 0 1