∀ {D : Type u_3} {C : Type u_4} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{u_2, u_4} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (F X : CategoryTheory.Functor D C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorLeft F).map (F.closedUnit.app X))
      (F.closedCounit.app ((CategoryTheory.MonoidalCategory.tensorLeft F).obj X)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorLeft F).obj X)