{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        {motive : S.RightHomologyData → Sort u} →
          (t : S.RightHomologyData) →
            ((Q H : C) →
                (p : S.X₂ ⟶ Q) →
                  (ι : H ⟶ Q) →
                    (wp : CategoryTheory.CategoryStruct.comp S.f p = 0) →
                      (hp : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p wp)) →
                        (wι :
                            CategoryTheory.CategoryStruct.comp ι
                                (hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) =
                              0) →
                          (hι : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι wι)) →
                            motive { Q := Q, H := H, p := p, ι := ι, wp := wp, hp := hp, wι := wι, hι := hι }) →
              motive t