∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X₁ X₂ X₃ : C} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (zero : autoParam (CategoryTheory.CategoryStruct.comp f g = 0) CategoryTheory.ShortComplex.zero._autoParam)
  (X₁_1 X₂_1 X₃_1 : C) (f_1 : X₁_1 ⟶ X₂_1) (g_1 : X₂_1 ⟶ X₃_1)
  (zero_1 : autoParam (CategoryTheory.CategoryStruct.comp f_1 g_1 = 0) CategoryTheory.ShortComplex.zero._autoParam),
  ({ X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f, g := g, zero := zero } =
      { X₁ := X₁_1, X₂ := X₂_1, X₃ := X₃_1, f := f_1, g := g_1, zero := zero_1 }) =
    (X₁ = X₁_1 ∧ X₂ = X₂_1 ∧ X₃ = X₃_1 ∧ f ≍ f_1 ∧ g ≍ g_1)