[Agda] Termination not being proven

[Will Sonnex]

I have a structurally recursive function which checks whether a list
is sorted, but Agda tells me it cannot prove termination:

_<=_ : ℕ → ℕ → Bool
zero <= _ = true
suc x <= zero = false
suc x <= suc y = x <= y

sorted : List ℕ → Bool
sorted [] = true
sorted (_ ∷ []) = true
sorted (x ∷ (y ∷ ys)) with x <= y
... | true = sorted (y ∷ ys)
... | false = false


It seems strange to me that Agda can show "xs ≺ x :: xs" but not "y ::
ys ≺ x :: (y :: ys)", since the former is a more general case of the
latter.


Cheers,

Will