∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n} (self : S.Exact) (i : ℕ)
  (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.Exact._auto_1), (S.sc ⋯ i hi).Exact