/*
{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:int | n > 0}
  record <'a> list(n) {
    head: 'a;
    tail: <'a> list(n-1)
  }
}
*/

record <'a> list {
  head: 'a;
  tail: <'a> list
}