∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X X' Y Z : C} (f : X ⟶ W) (g : Y ⟶ X) (f' : X' ⟶ W)
  (g' : Y ⟶ X') (h : Y ≅ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h.inv g) f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h.inv g') f' ↔
    CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp g' f'