Hi Serge, You can use the Acc data type in Induction.WellFounded to explicitly prove to Agda that your recursion terminates. At the risk of tooting my own horn, here is a post I wrote on this topic a few weeks back: http://playingwithpointers.com/archives/867 Cheers! -- Sanjoy Das http://playingwithpointers.com