∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} 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),
  CategoryTheory.CategoryStruct.comp
        (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)
        right.hom =
      CategoryTheory.CategoryStruct.comp left.hom
        (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5) →
    CategoryTheory.CategoryStruct.comp
        (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)
        right.inv =
      CategoryTheory.CategoryStruct.comp left.inv
        (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)