∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y)
  (h' : Z = X),
  f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h)
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom h')) ↔
    f ≍ g