Add rewrites for `seq.update`/`seq.nth` (#7966)

Add rewrites for `seq.update`/`seq.nth` (#7966)

This commit adds rewrites for `seq.update` and `seq.nth`. It adds a
rewrite to check if an update is out of bounds and it adds rewrites to
evaluate these operators using `stripSymbolicLength()`. This allows us
for example to evaluate updates on concatenations of non-constant
`seq.unit`s.