val N:ℕ;
val M:ℕ;

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

proc has(a:array,n:index,x:elem):Bool
{
  var r:Bool ≔ ⊥;
  for var i:index ≔ 0; i < n ∧ ¬r; i ≔ i+1 do
  {
    if a[i] = x then r ≔ ⊤;
  }
  return r;
}

proc toset(a:array,n:index):Record[a:array,n:index]
{
  var b:array = Array[N,elem](0);
  var ia:index ≔ 0;
  var ib:index ≔ 0;
  while ia < n do
  {
    if ¬has(b,ib,a[ia]) then
    {
      b[ib] ≔ a[ia];
      ib ≔ ib+1;
    }
    ia ≔ ia+1;
  }
  return ⟨a:b,n:ib⟩;
}