Lambda calculus defining terms according to description I'm working on a problem I stumbled across online.
The goal is to define terms for two use cases which are defined as follows:
lists are encoded as:
$ [N_1,N_2,...,N_k] ≜ λc.λn.c N_1 (c N_2 (...(c N_k n)...)) $
$ head [N, . . . ] → _\beta^* N \\ $
$ empty [ ] →_\beta^* true \\ $
$ empty [N, . . . ] →\beta^* false $
With a note that head[] can reduce to whatever I want. Any idea how to define such terms?
 A: Below, I will write definitions on the form $\mathsf{foo}(x_1,\ldots,x_n)=e$ as syntactic sugar for $\mathsf{foo}=\lambda x_1.\cdots.\lambda x_n.e$ and expressions on the form $\mathsf{foo}(e_1,\ldots,e_n)$ as syntactic sugar for $\mathsf{foo}\ e_1\ \ldots\ e_n$.
List constructors:

*

*$\mathsf{nil} = \lambda c.\lambda n.n$

*$\mathsf{cons}(x,l) = \lambda c.\lambda n.c\ x\ (l\ c\ n)$
By these we have for example
$$\begin{align}
\mathsf{cons}(N_1, \mathsf{nil}) 
&= \lambda c.\lambda n.c\ N_1\ (\mathsf{nil}\ c\ n)
\to_\beta \lambda c.\lambda n.c\ N_1\ n
\\
\mathsf{cons}(N_1, \mathsf{cons}(N_2, \mathsf{nil}))
&= \lambda c.\lambda n.c\ N_1\ (\mathsf{cons}(N_2, \mathsf{nil})\ c\ n)
\\
&= \lambda c.\lambda n.c\ N_1\ ((\lambda c'.\lambda n'.c'\ N_2\ n')\ c\ n)
\\
&\to_\beta \lambda c.\lambda n.c\ N_1\ (c\ N_2\ n)
\end{align}$$
To get the head of a list, we need to find some function $c_{\mathsf{head}}$ and some value $n$ such that $\mathsf{cons}(x,l)\ c_{\mathsf{head}}\ n$ reduces to $x$. But
$$
\mathsf{cons}(x,l)\ c_{\mathsf{head}}\ n 
= (\lambda c'.\lambda n'.c'\ x\ (l\ c'\ n'))\ c_{\mathsf{head}}\ n 
\to_\beta c_{\mathsf{head}}\ x\ (l\ c'\ n)
$$
so we see that we can just take $c_{\mathsf{head}} = \lambda x.\lambda r.x$ and the value of $n$ doesn't matter.
Therefore, we can take
$$
\mathsf{head}(l) = l\ (\lambda x.\lambda r.x)\ \mathsf{id}
$$
where $\mathsf{id}(x)=x$.
To check if a list is empty, we need to find some function $c_{\mathsf{empty}}$ and some value $n$ such that $\mathsf{nil}\ c_{\mathsf{empty}}\ n$ reduces to $\mathsf{true}$, while $\mathsf{cons}(x,l)\ c_{\mathsf{empty}}\ n$ reduces to $\mathsf{false}$. But
$$
\mathsf{nil}\ c_{\mathsf{empty}}\ n 
= (\lambda c'.\lambda n'.n')\ c_{\mathsf{empty}}\ n
\to_\beta n
$$
and
$$
\mathsf{cons}(x,l)\ c_{\mathsf{empty}}\ n 
= (\lambda c'.\lambda n'.c'\ x\ (l\ c'\ n'))\ c_{\mathsf{empty}}\ n
\to_\beta c_{\mathsf{empty}}\ x\ (l\ c_{\mathsf{empty}}\ n)
.
$$
Note that the result for $\mathsf{nil}$ equals $n$ so we can take $n=\mathsf{true}$, and the result for $\mathsf{cons}(x,l)$ is an application of $c_{\mathsf{empty}}$ so we can just let $c_{\mathsf{empty}}\ x\ r$ return $\mathsf{false}.$ We therefore define
$$
\mathsf{empty}(l) = l\ (\lambda x.\lambda r.\mathsf{false})\ \mathsf{true}
$$

Showing that $\mathsf{head}\ (\mathsf{cons}\ a\ l) \to_\beta^* a$:
$$\begin{align}
\mathsf{head}\ (\mathsf{cons}\ a\ l)
&= (\lambda l'.l'\ (\lambda x.\lambda r.x)\ \mathsf{id})\ (\mathsf{cons}\ a\ l) \\
&\to_\beta (\mathsf{cons}\ a\ l)\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&= ((\lambda x'.\lambda l'.\lambda c.\lambda n.c\ x'\ (l'\ c\ n))\ a\ l)\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&= (\lambda x'.\lambda l'.\lambda c.\lambda n.c\ x'\ (l'\ c\ n))\ a\ l\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&\to_\beta (\lambda l'.\lambda c.\lambda n.c\ a\ (l'\ c\ n))\ l\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&\to_\beta (\lambda c.\lambda n.c\ a\ (l\ c\ n))\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&\to_\beta (\lambda n.(\lambda x.\lambda r.x)\ a\ (l\ (\lambda x.\lambda r.x)\ n))\ \mathsf{id} \\
&\to_\beta (\lambda x.\lambda r.x)\ a\ (l\ (\lambda x.\lambda r.x)\ \mathsf{id})) \\
&\to_\beta (\lambda r.a)\ (l\ (\lambda x.\lambda r.x)\ \mathsf{id})) \\
&\to_\beta a \\
\end{align}$$
