∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cocycle K L n) (a n' : ℤ) (hn' : n' + a = n),
  CochainComplex.HomComplex.δ n' (n' + 1) ((↑γ).rightShift a n' hn') = 0