Agda 2.3.2.1 kann nicht erkennen, dass die folgende Funktion beendet wird:

open import Data.Nat
open import Data.List
open import Relation.Nullary

merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes p = x ∷ merge xs (y ∷ ys)
... | _     = y ∷ merge (x ∷ xs) ys 
merge xs ys = xs ++ ys

Das Agda-Wiki sagt, dass es für den Termination Checker in Ordnung ist, wenn die Argumente bei rekursiven Aufrufen lexikografisch abnehmen. Basierend darauf scheint es, dass diese Funktion auch bestehen sollte. Was vermisse ich hier? Ist es auch in früheren Versionen von Agda in Ordnung? Ich habe ähnlichen Code im Internet gesehen und niemand erwähnte dort Kündigungsprobleme.