Lambda Calculus: Proving exponent property by induction Recently I have learned that given Church numerals $\bar n = \lambda fx.f^n x$ and $\bar m = \lambda fx.f^m x$, we can calculate $\overline{m^n}$ by applying $\exp=\lambda mn.nm$. I believe this means $\bar n \bar m$ can be evaluated to $\overline {m^n} = \lambda fx.f^{(m^n)} x$, and my idea is that this could be proven with induction.
I think by substituting $\bar m$ for $\bar n$ and following specific evaluations we can get $\overline {m-1}$, but I failed on every try.
How could I prove that this property holds? Any advice will be appreciated.
 A: The natural approach is to prove that $\overline{n} \, \overline{m} =_{\beta\eta} \overline{m^n}$ is by induction on $n \in \mathbb{N}$ (where $=_{\beta\eta}$ is the union of $\beta$-equivalence $=_\beta$ and $\eta$-equivalence $=_\eta$). But if you do that, the proof in the inductive case is quite convoluted, essentially because the inductive hypothesis is not strong enough.
My approach is to prove that property as a consequence of the two lemmas below, each of them proved by induction. Probably there are smarter and more elegant approaches, but unfortunately I am not aware of them.
Notation. Given two $\lambda$-terms $M, N$ and $m\in \mathbb{N}$, we set
\begin{align}
M^m N = \underbrace{M ( \dots (M}_{m \text{ times}} N) \dots )
\end{align}
in particular, $M^0N = N$, $M^1N = MN$, $M^2N = M(MN)$, $M^3N = M(M(MN))$.

Lemma 1. For all $m,n,k \in \mathbb{N}$, $(\lambda y.x^my)^n(x^kz) =_\beta x^{nm+k} z$ (note that, for $k = 0$, this means $(\lambda y.x^my)^nz =_\beta x^{nm} z$).
Proof. By induction on $n \in \mathbb{N}$.

*

*Base case. For $n = 0$, we have
\begin{align}
(\lambda y.x^my)^0(x^kz) = x^kz = x^{0m + k}z.
\end{align}


*Inductive case. Let $n \in \mathbb{N}$ and suppose that $(\lambda y.x^my)^n(x^kz) =_\beta x^{nm+k} z$ (inductive hypothesis). Let us show that $(\lambda y.x^my)^{n+1}(x^kz) =_\beta x^{(n+1)m+k} z$.
\begin{align}
(\lambda y.x^my)^{n+1}(x^kz) &= (\lambda y.x^my)^{n}((\lambda y.x^my)(x^kz))
\\
&=_\beta (\lambda y.x^my)^{n}(x^m(x^kz))
\\
&= (\lambda y.x^my)^{n}(x^{m+k}z)
\\
&=_{\beta} x^{nm+m+k}z  &\text{(by inductive hypothesis)}  
\\
&= x^{(n+1)m+k}z. &  \square
\end{align}

Lemma 2. For all $m,n \in \mathbb{N}$, $\overline{m}^n x =_{\beta\eta} \overline{m^n} x$.
Proof. By induciton on $n \in \mathbb{N}$.

*

*Base case. For $n = 0$, we have
\begin{align}
\overline{m}^0 x &= x 
\\
&=_\eta \lambda y. xy 
\\
&=_\beta (\lambda f.\lambda y.fy)x 
\\
&= \overline{1} x = \overline{m^0} x.
\end{align}


*Inductive case. Let $n \in \mathbb{N}$ and suppose that $\overline{m}^n x =_{\beta\eta} \overline{m^n} x$ (inductive hypothesis). Let us show that $\overline{m}^{n+1} x =_{\beta\eta} \overline{m^{n+1}} x$.
\begin{align}
\overline{m}^{n+1} x &= \overline{m}(\overline{m}^n x)
\\
&=_{\beta\eta} \overline{m} (\overline{m^n} x) &\text{(by inductive hypothesis)}
\\
&=  \overline{m} ( (\lambda f. \lambda y.f^{(m^n)}y) x)
\\
&=_\beta \overline{m} ( \lambda y.x^{(m^n)}y) 
\\
&= (\lambda f. \lambda z. f^m z) ( \lambda y.x^{(m^n)}y) 
\\
&=_\beta \lambda z. ( \lambda y.x^{(m^n)}y)^m z 
\\
&=_\beta \lambda z. x^{m\, m^n}z &\text{(by Lemma 1, applied with $k = 0$)}
\\
&= \lambda z. x^{(m^{n+1})}z
\\
&=_\beta (\lambda f. \lambda z. f^{(m^{n+1})}z)x = \overline{m^{n+1}} x. &\square
\end{align}

Finally, thanks to Lemma 2 (which is in turn proved by means of Lemma 1), we can easily prove that $\overline{n} \, \overline{m} =_{\beta\eta} \overline{m^n}$ for all $m,n \in \mathbb{N}$.
Indeed,
\begin{align}
\overline{n} \, \overline{m} &= (\lambda f. \lambda x. f^n x)\overline{m}
\\
&=_\beta \lambda x. \overline{m}^n x
\\
&=_{\beta\eta} \lambda x. \overline{m^n} x &\text{(by Lemma 2)}
\\
&=_\eta \overline{m^n}.
\end{align}

Technical remark (advanced). To prove that, for all $m,n \in \mathbb{N}$, $\overline{n} \, \overline{m}$ and $\overline{m^n}$ are equivalent, $\beta$-equivalence $=_\beta$ alone is not enough and the presence of $\eta$-equivalence $=_\eta$ is also mandatory. That is, $\overline{n} \, \overline{m} =_{\beta\eta} \overline{m^n}$ and we cannot replace $=_{\beta\eta}$ with a smaller equivalence relation. Indeed, consider the case $n = 0$:
\begin{align}
\overline{0} \, \overline{m} &= (\lambda f \lambda x.x) \, \overline{m} 
\\
&=_\beta \lambda x. x
\\
&=_\eta \lambda x .\lambda y. xy \\
&= \overline{1} = \overline{m⁰}
\end{align}
The only way to pass from $\lambda x.x$ to $\overline{1}$ is through $=_\eta$, since $\lambda x.x$ and $\overline{1}$ are distinct $\beta$-normal forms.
