∀ (C : Type u) (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) (a : C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C (CategoryTheory.FreeMonoidalCategory.of a) x =
    CategoryTheory.Iso.refl
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.FreeMonoidalCategory.inclusionObj x)
        (CategoryTheory.FreeMonoidalCategory.of a))