support for lexicograohic ordering

as a trivial example from tests/pos/lex.hs

```
{-@ Decrease foo 1 2 @-}
foo xs    (y:ys) = foo xs ys
foo (x:xs) ys    = foo xs ys
```

the rec type for foo is
```
foo :: xsr:[a] -> ysr::{v:[a] | (len xsr < len xs) \/ {(len v) < (len ys) /\ (len xsr) = (len xs)} } -> b
```

So, the decreasing arguments provided should be an increasing lists,