[Agda] list for termination counter

[Sergei Meshveliani]

Can somebody explain, please,
what may be a simple way to prove termination in the following example?

 
---------------------------------------------------------------
open import Function                   using (case_of_)
open import Algebra.FunctionProperties using (Op₂)
open import Relation.Nullary using (yes; no)
open import Relation.Binary  using (DecTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using(_≡_)
open import Data.Nat  using (ℕ; decTotalOrder)
open import Data.List using (List; []; _∷_)

open DecTotalOrder decTotalOrder using (_≤?_)

record R : Set where
               constructor r
               field  members : List ℕ

add : Op₂ R

add (r [])       g            =  g
add f            (r [])       =  f
add (r (m ∷ ms)) (r (n ∷ ns)) =
    case
        m ≤? n
    of \
    { (yes _) → let (r hMems) = add (r (m ∷ ms)) (r ns)
                in  r (n ∷ hMems)

    ; (no _)  → let (r hMems) = add (r ms) (r (n ∷ ns))
                in  r (m ∷ hMems)
    }
--------------------------------------------------------------------

This is something similar to merging of ordered lists.
Agda does not see termination. I think, this is due to that the lists
are kept under the constructor r.
So, I extract the two lists and use them as counters for termination:

-------------------------------------------------------------------
add f g =  aux f g (R.members f) (R.members g) PE.refl PE.refl
  where
  aux : (f g : R) → (ms ns : List ℕ) → ms ≡ R.members f →
                                       ns ≡ R.members g → R

  aux (r .[]) g        [] _  PE.refl _       =  g
  aux f       (r .[])  _  [] _       PE.refl =  f

  aux (r .(m ∷ ms)) (r .(n ∷ ns)) (m ∷ ms) (n ∷ ns) PE.refl PE.refl =
    case
        m ≤? n
    of \
    { (yes _) → let (r hMems) = aux (r (m ∷ ms)) (r ns) (m ∷ ms) ns
                                                        PE.refl PE.refl
                in  r (n ∷ hMems)

    ; (no _)  → let (r hMems) = aux (r ms) (r (n ∷ ns)) ms (n ∷ ns)
                                                        PE.refl PE.refl
                in  r (m ∷ hMems)
    }
------------------------------------------------------------------------

The 'yes' pattern calls aux with  ns  -- which list expression is
syntactically smaller than   n ∷ ns.
The 'no' pattern calls aux with  ms  -- which list expression is
syntactically smaller than   m ∷ ms.

But Agda still reports : "Termination checking failed".

Why?
How to fix?
What is a simple way to prove termination in this example?

Thanks,

------
Sergei