∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {sq₁ sq₂ : CategoryTheory.Square C} {τ₁ : sq₁.X₁ ⟶ sq₂.X₁}
  {τ₂ : sq₁.X₂ ⟶ sq₂.X₂} {τ₃ : sq₁.X₃ ⟶ sq₂.X₃} {τ₄ : sq₁.X₄ ⟶ sq₂.X₄}
  {comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₂)
      CategoryTheory.Square.Hom.comm₁₂._autoParam}
  {comm₁₃ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₃)
      CategoryTheory.Square.Hom.comm₁₃._autoParam}
  {comm₂₄ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₂ sq₂.f₂₄)
      CategoryTheory.Square.Hom.comm₂₄._autoParam}
  {comm₃₄ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₃ sq₂.f₃₄)
      CategoryTheory.Square.Hom.comm₃₄._autoParam}
  {τ₁_1 : sq₁.X₁ ⟶ sq₂.X₁} {τ₂_1 : sq₁.X₂ ⟶ sq₂.X₂} {τ₃_1 : sq₁.X₃ ⟶ sq₂.X₃} {τ₄_1 : sq₁.X₄ ⟶ sq₂.X₄}
  {comm₁₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂_1 = CategoryTheory.CategoryStruct.comp τ₁_1 sq₂.f₁₂)
      CategoryTheory.Square.Hom.comm₁₂._autoParam}
  {comm₁₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃_1 = CategoryTheory.CategoryStruct.comp τ₁_1 sq₂.f₁₃)
      CategoryTheory.Square.Hom.comm₁₃._autoParam}
  {comm₂₄_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄_1 = CategoryTheory.CategoryStruct.comp τ₂_1 sq₂.f₂₄)
      CategoryTheory.Square.Hom.comm₂₄._autoParam}
  {comm₃₄_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄_1 = CategoryTheory.CategoryStruct.comp τ₃_1 sq₂.f₃₄)
      CategoryTheory.Square.Hom.comm₃₄._autoParam},
  { τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, τ₄ := τ₄, comm₁₂ := comm₁₂, comm₁₃ := comm₁₃, comm₂₄ := comm₂₄, comm₃₄ := comm₃₄ } =
      { τ₁ := τ₁_1, τ₂ := τ₂_1, τ₃ := τ₃_1, τ₄ := τ₄_1, comm₁₂ := comm₁₂_1, comm₁₃ := comm₁₃_1, comm₂₄ := comm₂₄_1,
        comm₃₄ := comm₃₄_1 } →
    τ₁ = τ₁_1 ∧ τ₂ = τ₂_1 ∧ τ₃ = τ₃_1 ∧ τ₄ = τ₄_1