∀ {G : Type u_3} {H : Type u_1} {A : Type u_2} [inst : AddCommMonoid A] (e : G ≃ H) (a b : SkewMonoidAlgebra A G),
  SkewMonoidAlgebra.equivMapDomain e (a + b) =
    SkewMonoidAlgebra.equivMapDomain e a + SkewMonoidAlgebra.equivMapDomain e b