∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (i : ι),
  ¬c.Rel i (c.next i) → (dNext i) f = 0