∀ {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 j k : ℕ) (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.IsComplex.zero'._auto_1)
      (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.IsComplex.zero'._auto_3)
      (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.zero'._auto_5),
      CategoryTheory.CategoryStruct.comp (S.map' i j ⋯ ⋯) (S.map' j k ⋯ hk) = 0