val N:ℕ;
val M:ℕ;

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

pred hasPred(a:array,n:index,x:elem) ⇔
  ⊤
;

pred tosetPred(a:array,b:array,n:index) ⇔
  ⊤
;

proc has(a:array,n:index,x:elem):Bool
  ensures hasPred(a,n,x);
{
  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):Record[b:array,n:index]
  ensures tosetPred(a,result.b,result.n);
{
  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 ⟨b:b,n:ib⟩;
}