In Sorensen and Urzyczyn's book there is a lemma (1.3.11) which I am having a hard time proving.
1.3.11 Lemma:
If there is an infinite $\beta \eta$-reduction sequence starting with a term $M$ then there is an infinite $\beta$-reduction seqeunce from $M$.
Now the proof is sketched in the book but I am having trouble realising it:
Proof. First observe that in an infinite $\beta\eta$-reduction sequence there must be infinitely many $\beta$-reduction steps (cf. Exercise 1.6). These $\beta$-reduction steps can be "permuted forward", yielding an infinite $\beta$-reduction. Indeed, by induction with respect to $M \to_{\eta} N$, one can show that $M \to_{\eta}N \to_{\beta}L$ implies $M \to_\beta P \twoheadrightarrow_{\beta \eta} L$, for some $P$.
So $\to_\eta$ is defined as the least compatible relation satisfying $\lambda x . f x \to_\eta f$. Where compatible means works with the syntax, i.e. $A \to B$ imples $M A \to M B$, $A M \to B M$ and $\lambda x . A \to \lambda x .B$.
The definition is similar for $\beta$ with the obvious reduction. The relation $\to_{\beta \eta}$ is the union of both. And $\twoheadrightarrow$ is the transitive-relfexive closure of said relation.
Exercise 1.6 was to prove that $\to_\eta$ is strongly normalising, which can be shown by considering a "depth" function on terms, and showing that this strictly decreases on $\eta$-reduction.
The problem I am having is I can't seem to understand how $\beta$ and $\eta$ interact.
Take for example $\lambda t. (\lambda x . y) t$. Clearly we can $\beta$-reduce this to get $\lambda t . y$ or $\eta$-reduce it to get $\lambda x . y$ which are clearly equal but its not obvious to me in general.
How can this be proven? And better yet, are there any references for this? I can't seem to find much on $\eta$-reduction in lambda calculus.