∀ {ι : Type u_3} {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (i : ι) (x x_1 : (i j : ι) → C.X i ⟶ D.X j),
  (x + x_1) (c.next i) i = (x + x_1) (c.next i) i