Map the library of sequences of Why3 to the SMTLIB theory of sequences
This mapping should follow the same guidelines as the mapping for functional mappings, or for bitvectors, or for character strings.
Caution must be taken for functions which are declared total in SMTLIB: the one for extracting a sub-sequence returns the empty sequence when the parameters are out of bounds, and the one for updating, which returns the sequence unchanged when out-of-bounds.