array(length0, length1) -- two-dimensional immutable array

array provides two-dimensional immutable arrays. These are actually
one-dimensional immutable arrays with an additional access function with
two index parameters.

pre
  safety: length0 ≥ 0
  safety: length1 ≥ 0
  safety: length0.as_i64 *? length1.as_i64 >=? 0
  debug : length0.fits_in_i64
  debug : length1.fits_in_i64