[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

I'm new to Agda and I'm having a problem which might seem rather basic. Let's say I have defined 
Nat, Bool, List, if_then_else_ and < operator that takes two Nats and returns true or false. Now 
I have something like this:

fun : List Nat -> List Nat -> List Nat
fun (x :: xs) (y :: ys) with x < y
fun (x :: xs) (y :: ys) | true  = ... (recursive call to fun)
fun (x :: xs) (y :: ys) | false = ... (recursive call to fun)

When I C-c C-l this code then name of the function in type signature as well as names of recursive 
calls are highlighted by Agda. No error is reported, just highlighting. If I however write 
something like this:

fun (x :: xs) (y :: ys) = 
    if x < y
    then ... (recursive call to fun)
    else ... (recursive call to fun)

then all works fine. According to Agda wiki this is related to termination checking, but I don't 
understand why the same code works perfectly with if-then-else but doesn't work with "with" 
construct. How can I use "with" and recursive calls together so that termination checker does not 
complain?

Janek