Add a sequence type: finitary arrays from natural numbers to some type

[vkuncak]

Modeling Scala arrays and lists currently does not work in cvc5 and it works badly in z3 as well when sequences are nested.

To remedy this, we should add a new type of finitary sequences.

Unlike arrays, finitary sequences admit induction principle, which we used extensively in reasoning about lists.

To see how e.g. cvc solvers can support this, chek https://arxiv.org/pdf/2205.08095

Princess has also various support for such sequences, much of this work is driven by reasoning about strings but the techniques handle arbitrary codomains. In contrast, we do not need domain to be anything other than non-negative integers.