∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Abelian C] {ι' : Type u_3}
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ →
    ∀ (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂),
      CategoryTheory.Limits.IsZero ((X'.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE h₀₁))) →
        CategoryTheory.Epi ((X'.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))