Support SMT theory of Sequences
It would be nice to leverage the support for sequences increasingly found in major SMT solvers like Z3, and CVC5.
The theory used by CVC5 is documented here: https://arxiv.org/pdf/2205.08095.pdf while Z3 uses the same one without update
(which can be built from the remaining primitives).