∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cochain M K n),
  α = α_1 →
    ∀ (β β_1 : CochainComplex.HomComplex.Cochain M L m),
      β = β_1 →
        ∀ (h : m + 1 = n) (T : CochainComplex.HomComplex.Triplet n),
          CochainComplex.mappingCocone.liftCochain φ α β h T = CochainComplex.mappingCocone.liftCochain φ α_1 β_1 h T