the model is a sequence of integers, of type 'seq int'
the idea is to lower the pollution of VCs with values of int63 (and
subsequent to_int operations)

drawbacks:
- this new type of arrays is not compatible with the one
  from mach.array.Array63
- when using both, we cannot use syntax [] and []<- for both types
  in programs (no overloading in programs) and thus we have to use
  A.([]) and A.([]<-) for one of them