∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f g : C ≌ D} (α : e.functor ⟶ f.functor) (β : f.functor ⟶ g.functor) {Z : C ≌ D} (h : g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom (CategoryTheory.CategoryStruct.comp α β)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom α)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom β) h)