∀ {B : Type u_1} {B' : Type u_2} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W)
  (e : B ≃ B'), (cs.reindex e).mulEquiv = cs.mulEquiv.trans (M.reindexGroupEquiv e).symm