Is this Church encoding of lists correct? Types and Programming Languages by Pierce introduces Church encoding of lists in Exercise  5.2.8 on p63 and p500:
nil = λc. λn. n;
cons = λh. λt. λc. λn. c h (t c n);
head = λl. l (λh.λt.h) fls;
tail = λl.
        fst (l (λx. λp. pair (snd p) (cons x (snd p)))
            (pair nil nil));
isnil = λl. l (λh.λt.fls) tru;

Is fls in head correct? If I am corrrect, fls is Church encoding of Boolean value false.
Thanks.
 A: Yes, $\mathsf {fls}$ is correct.
The reason is the following. If $l$ is a list of the form $\mathsf {cons}\, h\, t$, then we want $\mathsf {head}\, l$ to reduce to $h$. But if $l$ is the list $\mathsf {nil}$, then $\mathsf {head}\, l$ should be undefined. In untyped lambda-calculus, we can define $\mathsf {head}$ so that $\mathsf {head}\, \mathsf {nil}$ reduces to $\mathsf {fls}$, the Boolean value false.
You can check now that the definition is correct:
\begin{align*}
\mathsf {head}\, (\mathsf {cons}\, h\, t) & = (\lambda l. l \, (\lambda h. \lambda t. h) \, \mathsf {fls}) (\mathsf {cons}\, h\, t) \\
& \to (\lambda l. l \, (\lambda h. \lambda t. h) \, \mathsf {fls}) (\lambda c. \lambda n. c\, h\, (t\, c\, n)) \\
& \to (\lambda c. \lambda n. c\, h\, (t\, c\, n)) (\lambda h. \lambda t. h) \, \mathsf {fls} \\
& \to (\lambda n. (\lambda h. \lambda t. h) h (t \, (\lambda h. \lambda t. h)\, n)) \, \mathsf {fls} \\
& \to (\lambda h. \lambda t. h) h (t \, (\lambda h. \lambda t. h) \, \mathsf {fls}) \\
& \to (\lambda t. h) (t \, (\lambda h. \lambda t. h) \, \mathsf {fls}) \\
& \to h
\end{align*}
\begin{align*}
\mathsf {head} \, \mathsf {nil} & = (\lambda l. l \, (\lambda h. \lambda t. h) \, \mathsf {fls}) \, \mathsf {nil} \\
& = (\lambda l. l \, (\lambda h. \lambda t. h) \, \mathsf {fls}) \, \mathsf (\lambda c. \lambda n. n) \\
& \to (\lambda c. \lambda n. n) (\lambda h. \lambda t. h) \, \mathsf {fls} \\
& \to (\lambda n. n) \, \mathsf {fls} \\
& \to \mathsf {fls}
\end{align*}
