∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] (i j i' j' n : ℕ) (x : i ≤ j) (x_1 : i' ≤ j')
  (x_2 : i ≤ i') (x_3 : j ≤ j') (x_4 : j' ≤ n) (S : CategoryTheory.ComposableArrows C n),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.ComposableArrows.functorArrows C i j n ⋯ ⋯).obj S).map' 0 1
        CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)
      (S.map' j j' x_3 x_4) =
    CategoryTheory.CategoryStruct.comp (S.map' i i' x_2 ⋯)
      (((CategoryTheory.ComposableArrows.functorArrows C i' j' n ⋯ ⋯).obj S).map' 0 1
        CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)