[Agda] termination for nested construct

[Sergei Meshveliani]

People,
I have a recursion of kind 

 f : Foo → Set    
 f (foo (foo' (x ∷ xs) prop'-x:xs) prop-x:xs) = ... 
                              where 
                              d = f (foo (foo' xs prop'-xs) prop-xs)
                              ..., 

where  foo  and  foo'  are the two record constructors, and recursion is
by changing  x :: xs  -->  xs.

Agda-2.4.2.2 does not see termination here.

What is the simplest method to prove termination for f ?


I apply the following approach. Extract  xs  from the Foo data and use
it as an additional argument in 'prove'. But this needs also to equate
this argument in `prove' to the list in the Foo data. So that the
function becomes

 f (foo (foo' xs prop') prop) =                   
                        prove (foo (foo' xs prop') prop) xs PE.refl    
   where 
   prove : (d : Foo) → (xs : List C) → list d ≡ xs → Set 

   prove _ [] _ =  =foo-refl      
   prove (foo (foo' (x ∷ xs) prop'x:xs) prop-x:xs) 
                                        (.x ∷ .xs) PE.refl =  ...
         where 
         ...  prove (foo (foo' xs prop'xs) prop-xs) xs PE.refl


Is there possible a simpler method?

Thanks,

------
Sergei