val N:ℕ;
val M:ℕ; 

type int   = ℤ[-1,N];
type elem  = ℕ[M];
type array = Array[N,elem];

// we construct from array "a" a new array as follows: we insert at
// position "p" element "x", shifting all elements at positions
// greater equal "p" one position to the right and dropping the last
// element (the new array has the same length as "a")
proc insert(a:array,p:int,x:elem): array
{
  var b:array = Array[N,elem](0);
  var i:int ≔ 0;
  while i < N do
  {
    if i < p then
      b[i] ≔ a[i];
    else if i = p then
      b[i] ≔ x;
    else
      b[i] ≔ a[i-1]; 
    i ≔ i+1;
  }
  return b;
}