∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} {x y : S₁.Hom S₂},
  x.f₀ = y.f₀ → x.f₁ = y.f₁ → x.f₂ = y.f₂ → x.f₃ = y.f₃ → x = y