Lambda the Ultimate

Ola Bini, a core JRuby developer and author of the book Practical JRuby on Rails Projects, has been developing a new language for the JVM called Ioke. This strongly typed, extremely dynamic, prototype based object oriented language aims to give developers the same kind of power they get with Lisp and Ruby, combined with a nice, small, regular syntax.

InfoQ has a Q&A with Ola about Ioke.

The process of programming language creation is a subject of too little reflection and retrospection. Newcomers to the field (including, in some measure, us) regularly propose new languages without quite understanding what they are getting into or how big the task is.
... This paper describes the motivation and early design evolution of the BitC programming language, making our excuses in hindsight and providing a compilation of some of the things that we learned along the way.
... The ML module system [18] is fully understood only by David MacQueen, and only on alternating weeks. The Scheme module system [8] required the combined brilliance of Matt Flatt and Matthias Felleisen (and six revisions of the language standard) to achieve. From the perspective of a mere operating systems weenie, it's all rather discouraging, but what is the reluctant programming language designer to do?
... The real reason we stuck with the LISP-ish syntax is that we didn't want to be fiddling with the parser while designing the language, and (to a lesser degree) because we didn't want to encourage programmers until we thought the language was ready.

The Origins of the BitC Programming Language Warning: Work in Progress

I was just struck with a minor revelation. The informal explanation for α-equivalence in λ-calculus is that a function "does the same thing" regardless of the particular names that we might choose for its internal variables. But this seems like just a particular case of the general extensionality principle!

Technically, α-conversion means that a bound variable may be renamed to another one as long as no free variables are captured:

    y ∉ FV(e)
―――――――――――――――――― (α)
λx. e = λy. e[y/x]

And indeed, it turns out that in the presence of the η-rule, which expresses the extensionality principle, the above rule is derivable:

y ∉ FV(e)
―――――――――――――       ―――――――――――――――――― (β)
y ∉ FV(λx. e)       (λx. e) y = e[y/x]
――――――――――――― (η)   ―――――――――――――――――― (ξ)
λx. e  =  λy. (λx. e) y  =  λy. e[y/x]

This is of course quite trivial. However, I've read a fair number of tutorials to λ-calculus, and I don't recall having ever seen this particular tidbit mentioned anywhere. I'm unsure whether this is because I just haven't read the right papers, or the matter is so trivial that no one bothers mentioning it explicitly, or there's something wrong with my reasoning.

So, just to ease my mind, could someone please either direct me to some respectable source where the redundancy of α in the presence of η is confirmed, or else point out what I'm missing here?

Thanks.