∀ {C : Type u} (a : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) (a_1 : C)
  (a_2 : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) (a_3 : C),
  (a.tensor a_1 = a_2.tensor a_3) = (a = a_2 ∧ a_1 = a_3)