∀ (C : Type u) (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C CategoryTheory.FreeMonoidalCategory.unit x =
    CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.inclusionObj x)