∀ {B : Type u_1} (M : Matrix B B ℕ) (isSymm : autoParam M.IsSymm CoxeterMatrix.isSymm._autoParam)
  (diagonal : autoParam (∀ (i : B), M i i = 1) CoxeterMatrix.diagonal._autoParam)
  (off_diagonal : autoParam (∀ (i i' : B), i ≠ i' → M i i' ≠ 1) CoxeterMatrix.off_diagonal._autoParam)
  (M_1 : Matrix B B ℕ) (isSymm_1 : autoParam M_1.IsSymm CoxeterMatrix.isSymm._autoParam)
  (diagonal_1 : autoParam (∀ (i : B), M_1 i i = 1) CoxeterMatrix.diagonal._autoParam)
  (off_diagonal_1 : autoParam (∀ (i i' : B), i ≠ i' → M_1 i i' ≠ 1) CoxeterMatrix.off_diagonal._autoParam),
  ({ M := M, isSymm := isSymm, diagonal := diagonal, off_diagonal := off_diagonal } =
      { M := M_1, isSymm := isSymm_1, diagonal := diagonal_1, off_diagonal := off_diagonal_1 }) =
    (M = M_1)