{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {F G : CategoryTheory.ComposableArrows C 1} →
      (left :
          F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⟶
            G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4) →
        (right :
            F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ⟶
              G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5) →
          autoParam
              (CategoryTheory.CategoryStruct.comp
                  (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4
                    CategoryTheory.ComposableArrows.homMk₁._proof_5)
                  right =
                CategoryTheory.CategoryStruct.comp left
                  (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4
                    CategoryTheory.ComposableArrows.homMk₁._proof_5))
              CategoryTheory.ComposableArrows.homMk₁._auto_1 →
            (F ⟶ G)