∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} (self : F.HomObj G A) {c d : C} (f : c ⟶ d)
  (a : A.obj c) {Z : D} (h : G.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (self.app d (A.map f a)) h) =
    CategoryTheory.CategoryStruct.comp (self.app c a) (CategoryTheory.CategoryStruct.comp (G.map f) h)