∀ {V : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ : V) (d₀ : X₁ ⟶ X₀)
  (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0),
  (ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X (0 + 2) =
    (succ' ((ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d (0 + 1) 0)).fst