∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnrichedOrdinary C}
  {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c),
  CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.CategoryStruct.comp η θ)
      (CategoryTheory.CategoryStruct.id i) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnrichedOrdinary.hComp η (CategoryTheory.CategoryStruct.id i))
      (CategoryTheory.CatEnrichedOrdinary.hComp θ (CategoryTheory.CategoryStruct.id i))