∀ {M : Type u_2} {N : Type u_3} {P : Type u_1} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] (f : M →+ N →+ P) (m₁ m₂ : M) (n : N),
  (FreeAddMonoid.lift fun mn => (f mn.1) mn.2) (FreeAddMonoid.of (m₁, n) + FreeAddMonoid.of (m₂, n)) =
    (FreeAddMonoid.lift fun mn => (f mn.1) mn.2) (FreeAddMonoid.of (m₁ + m₂, n))