[TYPES] Permutation of beta-redexes in lambda-calculus

["Stéphane Lengrand (Work)"]

Dear all,

I have recently found it necessary to prove the following theorem (by a 
series of adjournment properties), and was wondering if it rings a bell 
to anyone.

Definition: Let gamma be a new reduction rule of lambda-calculus defined as
(lambda x.M) ((lambda y.N) P) ---> (lambda y.(lambda x.M) N) P
(avoiding capture of y in M, obviously)

Theorem: If M is SN for beta, then M is SN for beta+gamma.

The rule comes up in my framework for a call-by-value evaluation similar 
to Moggi's lambdaC.
I'm sure that its termination (together with beta-reduction) must have 
already come up in someone else's work...

Stephane Lengrand
lengrand at lix.polytechnique.fr