∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h