∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₂ : f.obj' 2 _proof_355✝ ≅ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ≅ g.obj' 3 _proof_356✝¹),
  CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃.hom =
      CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝¹ _proof_356✝³) →
    CategoryTheory.CategoryStruct.comp (g.map' 2 3 _proof_291✝² _proof_356✝⁴) app₃.inv =
      CategoryTheory.CategoryStruct.comp app₂.inv (f.map' 2 3 _proof_291✝³ _proof_356✝⁵)