∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (D : CategoryTheory.GlueData' C) (i j k : D.J)
  (hij : i = j),
  CategoryTheory.CategoryStruct.comp (D.f' i k) (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (D.f' j k)