Infinite $\beta \eta$-reduction sequence implies infinite $\beta$-reduction sequence 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 &quot;permuted forward&quot;, 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 &quot;depth&quot; 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.
As usual, the bible knows all, and Lemma 3.3.8 (p 66) gives the detailed proof of commutativity of $\beta$ and $\eta$ reductions.

Trying to reproduce it here would be tedious and wouldn't do it justice, so I'll include a picture:



You had the main idea right, it just takes a bit of practice to generalize from the specific examples.