Introduce an operator for bounded sequences

[konnov]

This issue has been discussed in zulip, but also popped up several times before. TLA+ has the operator Seq(S), which produces a set of all sequences over a set S. The problem with this operator is that it produces an infinite set, and Apalache cannot handle that.

To solve this issue, we have two options:

1. Introduce an operator like ApaBoundedSeq(S, n), which takes an explicit upper bound n on the length of the sequences.
2. Introduce special treatment for { seq \in Seq(S): Len(seq) <= n }.

Actually, it may be a good idea to implement (2) and introduce (1) for discoverability of this pattern.