Dear Thorsten, :-)When proving properties about systems with bound variables it :-)simplifies notation and understandibility quite a lot when we use :-)de Bruijn's notation. Otherwise we end up mumbling the words "up to :-)alpha equivalence" like a mantra. Completely right, but you run the risk that for the outsider your remark that actually you use de Bruijn's notation may be interpreted as a mantra as well. :-)Recently I did a machine checked and complete formalisation of the :-)strong normalisation proof for System F using de Bruijn indices (LFCS :-)report 92-230). I find it very hard to imagine doing the same thing :-)with named variables. Indeed! I am intersted in receiving a copy of your report. What were the difficulties you encountered in making this machine checked proof? Did it take you a long time? many thanks in advance! (uuencoded dvi-version is also welcome...) Fer-Jan de Vries, Department of Software technology CWI Kruislaan 413 1098 SJ Amsterdam ferjan@cwi.nl ==============================================================================