{n:nat, i:nat | i < n}
record <'a> heap(n, i) {
  max: int(n);
  size: int(i);
  heap[n]: 'a
}

/*
?record <'a> list with nat {
  list(0);
  {n:nat}
  record <'a> list(n+1) {
    head: 'a;
    tail: 'a * <'a> list(n)
  }
}

('a){n:nat}
int(n) length (xs: <'a> list(n)) {
  var: int i;;

  i = 0;

  invariant:
    [i:int,j:nat | i+j = n] (i: int(i), xs: list(j))
  while (!null(xs)) {
    i = i + 1;
    xs = xs.tail;
  }
}

{m:nat,n:nat}
record <'a> sparse_array(m, n) {
  row: int(m);
  col: int(n);
  data[m]: <[i:nat | i < n] (int(i) * 'a)> list
}

{n:nat}
record <'a> array(n) {
  size: int(n);
  data[n]: 'a
}

{m:nat,n:nat}
record <'a> array2d(m, n) {
  row: int(m);
  col: int(n);
  data[m][n]: 'a
}

*/