Dear Andrzej: >One may only reduce a term to a subterm. Ah, that's quite restrictive! I wanted to tell my Coq friends about this (they always complain that Mizar has no reduction), but now I don't know whether I dare to :-) Freek