∀ (V : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {D : Type u_3} [inst_2 : CategoryTheory.EnrichedCategory V D] {X Y Z : CategoryTheory.ForgetEnrichment V D}
  (x : X ⟶ Y) (x_1 : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (x, x_1).1 (x, x_1).2))
      (CategoryTheory.eComp V X Y Z) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (x, x_1).1 (x, x_1).2)
        (CategoryTheory.eComp V X Y Z))