∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D] (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (((G.mapComposableArrows 2).obj (CategoryTheory.ComposableArrows.mk₂ f g)).map' 0 1
        CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_238✝)
      (CategoryTheory.Iso.refl
          (((G.mapComposableArrows 2).obj (CategoryTheory.ComposableArrows.mk₂ f g)).obj' 1 _proof_238✝¹)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          (((G.mapComposableArrows 2).obj (CategoryTheory.ComposableArrows.mk₂ f g)).obj' 0 _proof_237✝)).hom
      ((CategoryTheory.ComposableArrows.mk₂ (G.map f) (G.map g)).map' 0 1
        CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_238✝²)