[Agda] Termination proof in partiality monad

[Edsko de Vries]

Hi,

Suppose I give a definition of the partiality monad together with a  
simple fixed point operator (like in Edwin Brady's SK evaluator in  
Coq, http://www.cs.st-andrews.ac.uk/~eb/partial.php, or Dan Doel's  
definition in Agda, http://article.gmane.org/gmane.comp.lang.agda/ 
218). With such a definition, we can easily define recursive functions  
(for example, Dan Doel's factorial function).

Now I have a simple question: given an inductive characterization of  
termination, how would one prove that fac terminates? I have tried  
various approaches (in Coq) but am making no progress at all.

Any hints would be appreciated,

Edsko

PS. I asked this before on the Coq mailing list but received no  
replies; perhaps my previous email was too low-level. Hence this repost.