{B : Type u_1} →
  {motive : CoxeterMatrix B → Sort u} →
    ((M : Matrix B B ℕ) →
        (isSymm : M.IsSymm) →
          (diagonal : ∀ (i : B), M i i = 1) →
            (off_diagonal : ∀ (i i' : B), i ≠ i' → M i i' ≠ 1) →
              motive { M := M, isSymm := isSymm, diagonal := diagonal, off_diagonal := off_diagonal }) →
      (t : CoxeterMatrix B) → motive t