Lambda calculus - church encoding and lists I'm reading a book on the $\lambda$-calculus and I'm stuck on a list of representations. While practising different lambda calculus tasks I've stumbled upon an interesting issue. Given two terms I would like to understand what list is represented by those - or what is the actual process of transforming those.
I have two terms defined:
$F_n$ and $F'_n$ for each natural number $n \in \mathbb{N} $ is defined as following:

*

*$n$ is either a number or a Church encoding,

*$m$ and $c$ are variables.

$F'_0 = m$
$F'_n = c n F'_{n-1}$ for $n > 0$
$F_n =\lambda c. \lambda m.F'_n $
The question is what kind of list does the term $F_n$ represent?
Expanding a bit on the question as the context was marked as insufficient. Understanding how different lists are represented in lambda calculus is an important part of a learning process, moreover, I haven't found any great sources on how in the general process given terms into a specific list type. The provided answer nicely highlights the process of transitioning a term into an actual list representation.
 A: To understand the meaning of a family of terms defined by induction, my suggestion is to take some concrete examples.
So, let us see what are $F_0'$, $F_1'$, $F_2'$, $F_3'$, and $F_0$, $F_1$, $F_2$, $F_3$ (for every $n \in \mathbb{N}$, the Church numeral representing $n$ is denoted by $\underline{n}$)
\begin{align}
 F_0' &= m 
&
 F_0 &= \lambda c. \lambda m. m
\\
 F_1' &= c \underline{1} F_0' = c \, \underline{1} \, m 
&
 F_1 &= \lambda c. \lambda m. c \, \underline{1} \, F_0' = \lambda c. \lambda m. c \, \underline{1} \, m 
\\
 F_2' &= c \, \underline{2} \, F_1' = c \,\underline{2} (c \,\underline{1} \, m )
&
 F_2 &= \lambda c. \lambda m. c \,\underline{2} \, F_1' = \lambda c. \lambda m. c \, \underline{2} (c \, \underline{1} \, m )
\\
 F_3' &= c \, \underline{3} \, F_2' = c \, \underline{3} (c \, \underline{2} (c \, \underline{1} \, m ))
&
 F_3 &= \lambda c. \lambda m. c \, \underline{3} \, F_2' = \lambda c. \lambda m. c \, \underline{3} (c \, \underline{2} (c \, \underline{1} \, m ))
\\
\dots &
&
\dots
\\
 F_n' &= c \, \underline{n} \, F_{n-1}' = c \, \underline{n} (c \,\underline{n\!-\!1} \dots(c \, \underline{1} \, m ))
&
 F_n &= \lambda c. \lambda m. c \, \underline{n} \, F_{n-1}' = \lambda c. \lambda m. c \, \underline{n} (c \,\underline{n\!-\!1} \dots(c \, \underline{1} \, m ))
\end{align}
Now, as explained here and here, a list $[M_1, \dots, M_n]$ of $n \in \mathbb{N}$ "objects" can be represented in the $\lambda$-calculus by the term
$$\tag{$*$}
\lambda c.\lambda m.c M_1 (c M_2 (\dots(c M_n m)...))
$$
Comparing $(*)$ and $F_n$, it is clear that $F_n$ is nothing but the instance of $(*)$ where $M_1$ is replaced by $\underline{n}$, and $M_2$ is replaced by $\underline{n-1}$, and so on (in general, $M_k$ is replaced by $\underline{n-k+1}$, for all $1 \leq k \leq n$).
Therefore, for every $n \in \mathbb{N}$, the term
$$F_n = \lambda c. \lambda m. c \, \underline{n} (c \,\underline{n\!-\!1} \dots(c \, \underline{1} \, m ))$$
represents
$$[\,\underline{n}, \underline{n-1}, \dots, \underline{1}\,]$$ the decreasing list of natural numbers from $n$ to $1$.
