∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  {φ φ' : f ⟶ g},
  φ = φ' ↔
    CategoryTheory.ComposableArrows.app' φ 0 _proof_441✝ = CategoryTheory.ComposableArrows.app' φ' 0 _proof_441✝¹ ∧
      CategoryTheory.ComposableArrows.app' φ 1 _proof_442✝ = CategoryTheory.ComposableArrows.app' φ' 1 _proof_442✝¹ ∧
        CategoryTheory.ComposableArrows.app' φ 2 _proof_443✝ = CategoryTheory.ComposableArrows.app' φ' 2 _proof_443✝¹ ∧
          CategoryTheory.ComposableArrows.app' φ 3 _proof_444✝ =
              CategoryTheory.ComposableArrows.app' φ' 3 _proof_444✝¹ ∧
            CategoryTheory.ComposableArrows.app' φ 4 _proof_445✝ =
                CategoryTheory.ComposableArrows.app' φ' 4 _proof_445✝¹ ∧
              CategoryTheory.ComposableArrows.app' φ 5 _proof_446✝ =
                CategoryTheory.ComposableArrows.app' φ' 5 _proof_446✝¹