Proving terms using induction in LC Expanding on the following question here and on the book on the $\lambda$-calculus I'm reading, I'm trying to prove the correctness of the given solution in a more complicated manner.
Let $(F_n')_{n \in \mathbb{N}}$ be the family of terms defined by induction on $n \in \mathbb{N}$ as follows:
\begin{align}
F_0' &= m & F_{n+1}' &= c \, \underline{n+1} \, F_n'
\end{align}
where  $c$ and $m$ are variables, and $\underline{n}$ is the Church numeral representing $n \in \mathbb{N}$.
I'm trying to prove by induction on $n \in \mathbb{N}$ that $$F'_n[\mathsf{times}/c,\underline{1}/m] →_\beta^* \underline{n!}$$ and thus, by setting $F_n = \lambda c. \lambda m. F_n'$,
$$F_n \, \mathsf{times} \, \underline{1} →_\beta^* \underline{n!}$$
where $!$ is factorial, and $\mathsf{times}$ is a term such that $\mathsf{times} \, \underline{a} \, \underline{b} \to_\beta^* \underline{a \times b}$ for any $a, b \in \mathbb{N}$. How can I do it?
The proof should hopefully prove that the solution given in the previous question is valid and demonstrate the functionality of foldr function from haskell.
 A: It is possible to prove that, for every $n \in \mathbb{N}$, we have $F_n'[\mathsf{times}/c, \underline{n}/m] \to_\beta^* \underline{n!}$, by straightforward induction on $n \in \mathbb{N}$.

*

*Base case $n = 0$: By definition, $F_0' = m$ and so $F_0'[\mathsf{times}/c, \underline{1}/m] = \underline{1} = \underline{0!}$ (remember that $0! = 1$), and so $F_0'[\mathsf{times}/c, \underline{1}/m] \to_\beta^* \underline{0!}$ because $\to_\beta^*$ is a reflexive relation.


*Inductive case: Given $n \in \mathbb{N}$, we suppose that $F_n'[\mathsf{times}/c, \underline{n}/m] \to_\beta^* \underline{n!}$ (this is our inductive hypothesis) and we want to show that $F_{n+1}'[\mathsf{times}/c, \underline{n\!+\!1}/m] \to_\beta^* \underline{(n\!+\!1)!}$. By definition, $F_{n+1}' = c \, \underline{n\!+\!1} \, F_n'$ and hence
\begin{align}
F_{n+1}'[\mathsf{times}/c, \underline{n\!+\!1}/m] &= \mathsf{times} \, \underline{n\!+\!1} \, (F_n'[\mathsf{times}/c, \underline{n}/m])
\\
&\to_\beta^* \mathsf{times} \, \underline{n+1} \, \underline{n!} &&\text{(by inductive hypothesis)}
\\
&\to_\beta^* \underline{(n+1) \times n!} &&\text{(by definition of $\mathsf{times}$)}
\\
&= \underline{(n+1)!}
\end{align}
So, we have proved that, for every $n \in \mathbb{N}$,
$$\tag{$*$}
F_n'[\mathsf{times}/c, \underline{n}/m] \to_\beta^* \underline{n!}$$
As a consequence, $F_n \, \mathsf{times} \, \underline{1} \to_\beta^* \underline{n}$ for every $n \in \mathbb{N}$.
Indeed,
\begin{align}
F_n \, \mathsf{times} \, \underline{1} &= (\lambda c. \lambda m. F_n') \mathsf{times} \, \underline{1}
\\
&\to_\beta (\lambda m. F_n'[\mathsf{times}/c])\underline{1}
\\
&\to_\beta F_n'[\mathsf{times}/c, \underline{n}/m]
\\
&\to_\beta^* \underline{n!} &&\text{(by $(*)$)}
\end{align}
