[Agda] Interesting issue with termination checker

[Tom Cumming]

When the commented 'lem2' is swapped with the uncommented version agda
fails to prove termination. Could someone please shed some light as to
why:

reverse-inv : {A : Set} {n : ℕ} -> (xs : Vec A n) -> xs ≡ reverse (reverse xs)
reverse-inv [] = refl
reverse-inv (x ∷ xs) = sym (lem2 (lem x xs)) -- lem2 (lem x xs)
  where
    lem : {A : Set} {n : ℕ} -> (x : A) -> (xs : Vec A n) -> reverse (x
∷ xs) ≡ append (reverse xs) x
    lem x xs = refl

{- * This way cannot be proved to terminate
    lem2 : {A : Set} {n : ℕ} -> {xs ys : Vec A n} -> reverse xs ≡ ys
-> xs ≡ reverse ys
    lem2 {A} {n} {xs} {.(reverse xs)} refl = reverse-inv xs
-}

    lem2 : {A : Set} {n : ℕ} -> {xs ys : Vec A n} -> xs ≡ reverse ys
-> reverse xs ≡ ys
    lem2 {A} {n} {.(reverse xs)} {xs} refl = sym (reverse-inv xs)