∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {D : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_5, u_6} D] {E : Type u_8} [inst_2 : CategoryTheory.Category.{u_7, u_8} E]
  {E' : Type u_2} [inst_3 : CategoryTheory.Category.{u_1, u_2} E'] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (H : CategoryTheory.Functor E E') (x : C),
  (CategoryTheory.CategoryStruct.comp
          { app := fun x => CategoryTheory.CategoryStruct.id ((F.comp (G.comp H)).obj x), naturality := ⋯ }
          { app := fun x => CategoryTheory.CategoryStruct.id (((F.comp G).comp H).obj x), naturality := ⋯ }).app
      x =
    (CategoryTheory.CategoryStruct.id (F.comp (G.comp H))).app x