∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : FreeAddMonoid (M ⊕ N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0)
  (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0)
  (hM :
    ∀ (x y : M),
      f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y)))
  (hN :
    ∀ (x y : N),
      f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y)))
  (x : M), (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.inl x) = f (FreeAddMonoid.of (Sum.inl x))