{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {motive : CategoryTheory.ShortComplex.SnakeInput C → Sort u} →
        ((L₀ L₁ L₂ L₃ : CategoryTheory.ShortComplex C) →
            (v₀₁ : L₀ ⟶ L₁) →
              (v₁₂ : L₁ ⟶ L₂) →
                (v₂₃ : L₂ ⟶ L₃) →
                  (w₀₂ : CategoryTheory.CategoryStruct.comp v₀₁ v₁₂ = 0) →
                    (w₁₃ : CategoryTheory.CategoryStruct.comp v₁₂ v₂₃ = 0) →
                      (h₀ : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι v₀₁ w₀₂)) →
                        (h₃ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ v₂₃ w₁₃)) →
                          (L₁_exact : L₁.Exact) →
                            (epi_L₁_g : CategoryTheory.Epi L₁.g) →
                              (L₂_exact : L₂.Exact) →
                                (mono_L₂_f : CategoryTheory.Mono L₂.f) →
                                  motive
                                    { L₀ := L₀, L₁ := L₁, L₂ := L₂, L₃ := L₃, v₀₁ := v₀₁, v₁₂ := v₁₂, v₂₃ := v₂₃,
                                      w₀₂ := w₀₂, w₁₃ := w₁₃, h₀ := h₀, h₃ := h₃, L₁_exact := L₁_exact,
                                      epi_L₁_g := epi_L₁_g, L₂_exact := L₂_exact, mono_L₂_f := mono_L₂_f }) →
          (t : CategoryTheory.ShortComplex.SnakeInput C) → motive t