[TYPES] questiuon about strong normalization in untyped lambda-calculus

[Laurent Regnier]

> I have a proof of it in my 1994 TCS paper "Une équivalence sur les
> lambda-termes".

Sorry, I've been tricked by my memory, my paper proves a similar result but not
the strict lemma. A correct reference is Barendregt's book "The
lambda-calculus" where it is called the "Conservation theorem" (chapter 13
"Reduction strategies", in section 4 "An effective perpetual
strategy").

Laurent Regnier