∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : FreeMonoid (M ⊕ N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1)
  (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y)))
  (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y)))
  (w : FreeMonoid (M ⊕ N)), (Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.mk w) = f w