('a){m:nat,n:nat | n < m}
'a nth (xs: <'a> list(m), n: int(n)) {
   var: 'a x;;

   invariant: [m:nat, n:nat | n < m] (xs: <'a> list(m), n: int(n))
   while (true) {
     switch (xs) {
       case Cons(x, xs): if (n > 0) n = n - 1; else break;
     } 
   } withinv (x: 'a)

   return x;
}

('a){n:nat} int(n) length (xs: <'a> list(n)) {
  var: int x;;
  x = 0;
  invariant:
  [i:nat,j:nat | i+j=n] (xs: <'a> list(i), x: int(j))
  while (true) {
    switch(xs) {
      case Nil: break;
      case Cons(_, xs): x = x + 1;
    }
  } withinv (x: int(n))
  return x;
}

('a){m:nat,n:nat}
<'a> list(m+n) rev_append (xs: <'a> list(m), ys: <'a> list(n)) {
   var: 'a x;;
  
   invariant:
     [m1:nat,n1:nat | m1+n1 = m+n] (xs: <'a> list(m1), ys: <'a> list(n1))
   while (true) {
     switch (xs) {
       case Nil: break;
       case Cons(x, xs): ys = Cons(x, ys);
     }
   } withinv (ys: <'a> list(m+n))

   return ys;
}


/*
try { ... } with { ... } withinv { ... }
*/