∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)),
  Homotopy.nullHomotopicMap' h = Homotopy.nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0