By the way, why not M : \tau [ \gamma ]. Would allow to use a couple of other notations |- (M : \tau [ \gamma ]) I can prove that ... or (... |- M : \tau) [ \gamma ] In "context, environment,..." I can prove from ... that ... Axel Poigne ------------------------------------------------------ Axel Poigne GMD I5 - SKS Schloss Birlinghoven Tel. + 2241 142440 fax. + 2241 142618 Postfach 1316 email poigne@gmd.de D - 5205 Sankt Augustin 1