∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c d : CategoryTheory.CatEnriched C}
  (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)) η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToIso ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id f)
          (CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id g) η))
        (CategoryTheory.eqToIso ⋯).inv)