('a) {n:nat}
<'a> stack(n+1) push (x: 'a, s: <'a> stack(n)) {
  return stack {size = s.size+1; data = Cons (x, s.data) };
}

('a) {n:nat}
'a * <'a> stack(n) pop (s: <'a> stack(n+1)) {
  var: x: 'a; xs: <'a> list;;
  switch (s.data) {
    case Cons (x, xs): ;
  } withinv (x: 'a, xs: <'a> list(n))

  return (x, stack {size = s.size-1; data = xs});
}