[Agda] a termination problem

[Ramana Kumar]

Dear Agda Users

I've been playing around with Agda for a little while now, and would
like to get some feedback on the approach I'm taking, both generally
and in specific details.

So, if you see any bit of code that you would have written
differently, please let me know!

Apart from the feeling that "there must be a better way", I also have
a real problem to do with termination.
In particular, I define a recursive function that passes itself to
Relation.Binary.List.StrictLex.transitive.
How can I convince Agda that transitive will only apply it to smaller
arguments, or how can I avoid having to try?

My code is here http://hpaste.org/54675 (and the "Name" module here
http://hpaste.org/54676).

Thanks
Ramana