A verificação de término do Agda falhou para o exercício reverse-++-distrib

Eu estava fazendo um exercício de código em Agda do PLFA, para implementar uma prova de que "o reverso de uma lista anexada a outra é o reverso da segunda anexada ao reverso da primeira".

reverse-++-distrib : ∀ {A : Set} → (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

Consegui fazer os dois primeiros casos de indução sem problemas:

reverse-++-distrib {A} [] ys

reverse-++-distrib xs []

mas o terceiro passo tem um erro "Falha na verificação de terminação", o que eu acho que significa que o passo indutivo não foi feito corretamente.

reverse-++-distrib {A} (x :: xs) ys =
  begin
    reverse ((x :: xs) ++ ys)
  ≡⟨⟩
    reverse (x :: (xs ++ ys))
  ≡⟨⟩
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ (reverse xs ++ [ x ])
  ≡⟨ cong ((reverse ys) ++_) (cong ((reverse xs) ++_) (sym (reverse-++-fixed-point {A} x))) ⟩
    (reverse ys) ++ (reverse xs ++ (reverse [ x ]))
  **≡⟨ cong ((reverse ys) ++_) (sym (reverse-++-distrib {A} (x :: []) xs)) ⟩**
    (reverse ys) ++ (reverse ([ x ] ++ xs))
  ≡⟨⟩
    (reverse ys) ++ (reverse (x :: ([] ++ xs)))
  ≡⟨ cong ((reverse ys) ++_) (cong reverse (cong (x ::_) (++-identityˡ xs))) ⟩
    (reverse ys) ++ (reverse (x :: xs))
  ∎

A chamada problemática aparentemente é esta:

reverso-++-distribuição {A} (x :: []) xs

Para mim, isso parece bom porque o comprimento do primeiro argumento é 1, que é menor ou igual ao comprimento de x :: xs. E só é igual se xs for a lista vazia, caso em que deve entrar no segundo padrão de correspondência. Então, por que agda está tendo problemas com essa definição?