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.
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}