1. better handle the equality case, which is the reason for using a
   lexicographic order in the first place;
2. implement a proper lexicographic order, i.e., make (a,b) smaller
   than (a,b,c).

As a consequence of these two changes, in the following example, the VC
for f goes from (0 <= x /\ x < x) to true:

let rec f (x y : int) : int variant { x, () } = g x y
with g (x y : int) : int variant { x } = f (x-1) y