∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  (app₀ : f.obj' 0 _proof_237✝ ⟶ g.obj' 0 _proof_237✝¹) (app₁ : f.obj' 1 _proof_238✝ ⟶ g.obj' 1 _proof_238✝¹)
  (app₂ : f.obj' 2 _proof_239✝ ⟶ g.obj' 2 _proof_239✝¹)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_238✝²)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_238✝³))
      _auto_248✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_238✝⁴ _proof_239✝²) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝⁵ _proof_239✝³))
      _auto_250✝),
  (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁