∀ {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 ⟶ X (n + 1)) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0) (j : α),
  (CochainComplex.of X d sq).d j (j + 1) = d j