How can I prove a simple eta-conversion? I would like to prove the following:
$$\lambda x.\ \lambda y.\ f\ z\ x\ y \overset{\eta}{=} \lambda x.\ f\ z\ x$$
Definitions
Free variables
$x \in FV(f) :\Leftrightarrow$ $x$ is a variable used within a function $f$ and $x$ is neither a formal parameter of $f$ nor defined in the body of $f$.
$\alpha$-equivalence
Two terms $T_1, T_2$ are called $\alpha$-equivalent, if $T_1$ can be obtained from $T_2$ by consistant renaming.
$\beta$-equivalence
A $\beta$-reduction is function application on a redex:
$$(\lambda x. t_1)\ t_2 \Rightarrow t_1 [x \mapsto t_2]$$
$\eta$-equivalence
Two terms $\lambda x. f~x$ and $f$ are called $\eta$-equivalent, if $x \notin FV(f)$.
Some thoughts
I can make $\alpha$ conversions to get this:
$$\lambda y.\ \lambda x.\ g\ z\ y\ x \overset{\eta}{=} \lambda y.\ g\ z\ y$$
Then I could define $f := \lambda y.\ g\ z\ y$ so I had
$$\lambda y.\ \lambda x.\ g\ z\ y\ x \overset{\eta}{=} f$$
But now I have a problem. It seems as if I have to switch $\lambda y.\ \lambda x.\ \dots$ to $\lambda x.\ \lambda y.\ \dots$
May I do that? Is there a rule that tells me that this is a valid transformation?
 A: First of all, you can simplify the equation like this:
\begin{align*}
\lambda x.\ \lambda y.\ f\ z\ x\ y &\overset{!}{=} \lambda x.\ f\ z\ x\\
\overset{*}{\Leftrightarrow} \lambda y.\ f\ z\ x\ y &\overset{!}{=} f\ z\ x\\
\end{align*}
* is valid, because you may apply the rules to subterms. (Could somebody please go into detail here?)
Then you can make $\alpha$-conversions:
\begin{align*}
\lambda y.\ f\ z\ x\ y &\overset{!}{=} f\ z\ x\\
\overset{\alpha}{\Leftrightarrow} \lambda x.\ g\ z\ y\ x &\overset{!}{=} g\ z\ y
\end{align*}
Then you can define $f := g\ z\ y$:
\begin{align*}
\lambda x.\ g\ z\ y\ x &\overset{!}{=} g\ z\ y\\
\overset{f}{\Leftrightarrow} \lambda x.\ f\ x &\overset{!}{=} f
\end{align*}
The last line is true, because that's how $\eta$-conversion is defined. As we've used only equivalences, the other equations are true, too.
A: Let us consider $G=f\ z\ x$. Whence, $\lambda x.\lambda y. f\ z\ x\ y$ is syntactically the same as $\lambda x.\lambda y. G\ y$.
Now, $FV(G)=\{f,z,x\}$, so $y\notin FV(G)$. Therefore, $\lambda y. G\ y =_\eta G$. Therefore, $\lambda x.\lambda y. G\ y =_\eta \lambda x. G$.
If your trouble has to do with $G\ y$ being a subterm of $\lambda x. G\ y$, recall the definition of the $=_\eta$ relation: 


*

*$(\lambda x. M\ x) =_\eta M$, if $x\notin FV(M)$

*$M=_\eta M$

*$N=_\eta M$, if $M=_\eta N$

*$M=_\eta P$, if $M=_\eta N$ and $N=_\eta P$

*$\lambda x. M =_\eta \lambda x.N$, if $M=_\eta N$

*$MN =_\eta M'N$, if $M=_\eta M'$

*$MN = _\eta MN'$, if $N=_\eta N'$

A: The main problem seems to be that your definition descriptions are too narrow. For example, every lambda term is $\eta$-equivalent to itself (by the axiom of reflexivity), but your definition of $\eta$-equivalence only takes the $\eta$-axiom into account. The same criticism applies to your definition of $\beta$-equivalence, but this is not relevant here.
There are really only two rules in $\lambda\eta$ you need to use here. First of all, by axiom $\eta$ we have: 
$$(\lambda y.fzx y) = fzx \tag{1}$$
since $y \notin FV(fzx)$.
From both (1) and the rule of weak extensionality $\xi$ (a rule in $\lambda\eta$), defined as:
\begin{align}
M &\;= M' \\
\hline 
(\lambda x.M) &\;= (\lambda x.M')
\tag{$\xi$}
\end{align}
we can then infer $(\lambda x.\lambda y.fzxy) = (\lambda x. fzx)$.
