∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X (n + 1) ⟶ X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) {i j : α},
  i ≠ j + 1 → (ChainComplex.of X d sq).d i j = 0