Thanks Luke/Vladimir for your answers. I did try to weaken termination to a terminated_with relation, but I still get stuck. Vladimir, why do you think it might help? Luke, would you be able to show how far you got? I can't even massage the lemma into such a form that fac (S n) is expressed in terms of fac n.. Edsko