∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C),
  S.f = 0 →
    ∀ (c : CategoryTheory.Limits.KernelFork S.g) (hc : CategoryTheory.Limits.IsLimit c),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CategoryStruct.comp
            ((hc.ofIsoLimit (CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl c.pt) ⋯)).lift
              (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))
            (CategoryTheory.CategoryStruct.id c.pt))
          (CategoryTheory.Limits.Fork.ι c) =
        CategoryTheory.CategoryStruct.comp 0 (CategoryTheory.Limits.Fork.ι c)