∀ {V : Type u_4} [inst : CategoryTheory.Category.{u_2, u_4} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {C : Type u_1} [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u_3}
  [inst_3 : CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (h : F.forget ≅ G.forget),
  CategoryTheory.CategoryStruct.comp { out := h.hom } { out := h.inv } = CategoryTheory.CategoryStruct.id F