∀ (M : Type u_2) {R : Type u_1} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : Unique M]
  (x y : AddMonoidAlgebra R M),
  AddEquiv.finsuppUnique.toFun (x + y) = AddEquiv.finsuppUnique.toFun x + AddEquiv.finsuppUnique.toFun y