∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (f : S₁ ⟶ S₂) {Z : CochainComplex C ℤ} (h : S₂.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.descShortComplex S₂) h) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.descShortComplex S₁)
      (CategoryTheory.CategoryStruct.comp f.τ₃ h)