∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n},
  S.IsComplex →
    ∀ (i : ℕ) (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.IsComplex._auto_1) {Z : C}
      (h : S.obj ⟨i + 2, ⋯⟩ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (S.map' i (i + 1) ⋯ ⋯)
          (CategoryTheory.CategoryStruct.comp (S.map' (i + 1) (i + 2) ⋯ hi) h) =
        CategoryTheory.CategoryStruct.comp 0 h