{C : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} C} →
    {inst_1 : CategoryTheory.Preadditive C} →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} →
          {P : Sort u} →
            {h₀ : S₁.X₁ ⟶ S₂.X₁} →
              {h₀_f :
                  autoParam (CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0)
                    CategoryTheory.ShortComplex.Homotopy.h₀_f._autoParam} →
                {h₁ : S₁.X₂ ⟶ S₂.X₁} →
                  {h₂ : S₁.X₃ ⟶ S₂.X₂} →
                    {h₃ : S₁.X₃ ⟶ S₂.X₃} →
                      {g_h₃ :
                          autoParam (CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0)
                            CategoryTheory.ShortComplex.Homotopy.g_h₃._autoParam} →
                        {comm₁ :
                            autoParam (φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f h₁ + h₀ + φ₂.τ₁)
                              CategoryTheory.ShortComplex.Homotopy.comm₁._autoParam} →
                          {comm₂ :
                              autoParam
                                (φ₁.τ₂ =
                                  CategoryTheory.CategoryStruct.comp S₁.g h₂ +
                                      CategoryTheory.CategoryStruct.comp h₁ S₂.f +
                                    φ₂.τ₂)
                                CategoryTheory.ShortComplex.Homotopy.comm₂._autoParam} →
                            {comm₃ :
                                autoParam (φ₁.τ₃ = h₃ + CategoryTheory.CategoryStruct.comp h₂ S₂.g + φ₂.τ₃)
                                  CategoryTheory.ShortComplex.Homotopy.comm₃._autoParam} →
                              {h₀' : S₁.X₁ ⟶ S₂.X₁} →
                                {h₀_f' :
                                    autoParam (CategoryTheory.CategoryStruct.comp h₀' S₂.f = 0)
                                      CategoryTheory.ShortComplex.Homotopy.h₀_f._autoParam} →
                                  {h₁' : S₁.X₂ ⟶ S₂.X₁} →
                                    {h₂' : S₁.X₃ ⟶ S₂.X₂} →
                                      {h₃' : S₁.X₃ ⟶ S₂.X₃} →
                                        {g_h₃' :
                                            autoParam (CategoryTheory.CategoryStruct.comp S₁.g h₃' = 0)
                                              CategoryTheory.ShortComplex.Homotopy.g_h₃._autoParam} →
                                          {comm₁' :
                                              autoParam
                                                (φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f h₁' + h₀' + φ₂.τ₁)
                                                CategoryTheory.ShortComplex.Homotopy.comm₁._autoParam} →
                                            {comm₂' :
                                                autoParam
                                                  (φ₁.τ₂ =
                                                    CategoryTheory.CategoryStruct.comp S₁.g h₂' +
                                                        CategoryTheory.CategoryStruct.comp h₁' S₂.f +
                                                      φ₂.τ₂)
                                                  CategoryTheory.ShortComplex.Homotopy.comm₂._autoParam} →
                                              {comm₃' :
                                                  autoParam
                                                    (φ₁.τ₃ = h₃' + CategoryTheory.CategoryStruct.comp h₂' S₂.g + φ₂.τ₃)
                                                    CategoryTheory.ShortComplex.Homotopy.comm₃._autoParam} →
                                                { h₀ := h₀, h₀_f := h₀_f, h₁ := h₁, h₂ := h₂, h₃ := h₃, g_h₃ := g_h₃,
                                                      comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃ } =
                                                    { h₀ := h₀', h₀_f := h₀_f', h₁ := h₁', h₂ := h₂', h₃ := h₃',
                                                      g_h₃ := g_h₃', comm₁ := comm₁', comm₂ := comm₂',
                                                      comm₃ := comm₃' } →
                                                  (h₀ ≍ h₀' → h₁ ≍ h₁' → h₂ ≍ h₂' → h₃ ≍ h₃' → P) → P