∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {M : Type u_3} [inst_1 : AddZeroClass M]
  {f g : SkewMonoidAlgebra k G →+ M},
  (∀ (a : G) (b : k), f (SkewMonoidAlgebra.single a b) = g (SkewMonoidAlgebra.single a b)) → f = g