∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnrichedOrdinary C}
  {f f' : a ⟶ b} (α : f = f') {g g' : b ⟶ c} (β : g = g'),
  CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.eqToHom α) (CategoryTheory.eqToHom β) =
    CategoryTheory.eqToHom ⋯