∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₁ k₀ : ι},
  c.Rel k₁ k₀ →
    (∀ (l : ι), ¬c.Rel k₀ l) →
      ∀ (hom : (i j : ι) → C.X i ⟶ D.X j),
        (Homotopy.nullHomotopicMap hom).f k₀ = CategoryTheory.CategoryStruct.comp (hom k₀ k₁) (D.d k₁ k₀)