$[3,2,1]$ is just syntactic sugar for $\mathsf{cons} \, 3 \, (\mathsf{cons} \, 2 \, (\mathsf{cons} \, 1 \, \mathsf{nil}))$. $[3,2,1]$ is $\mathsf{cons} \, 3 \, [2,1]$ by definition of the $[\ldots]$ notation.
Because $\mathsf{cons}$ is part of the definition of lists, it isn't meaningful to ask whether $\mathsf{cons}$ is correct on its own. The meaningful question is whether the definition of lists is correct as a whole. (More precisely, that's the definition of an encoding of lists in the lambda calculus.) Another way to look at it is that the goal isn't to prove that the definition of cons
is correct, but that it's consistent with the rest of the definition of lists.
There are several, equivalent ways to define lists as an abstract type. Lists are an abstract type, defined by a number of functions and properties involving these functions. Lists are an abstract data type, so the functions can be classified into three groups: constructors (which build “bigger” lists from smaller lists and other stuff), destructors (which “break down” lists into smaller lists and other stuff) and other functions which can be built out of constructors and destructors. Any simple definition of lists uses two constructors: $\mathsf{nil}$ which is the empty list, and $\mathsf{cons}$ which takes two arguments, an element and a list, and returns a new list. The “most fundamental” (and easiest to reason with, but not easiest to understand) definition uses one destructor $\mathsf{case}$, and satisfies the following equations for any terms $f$, $g$, $h$, $t$ such that $t$ is a list:
$$
\begin{align}
\mathsf{case}\,\mathsf{nil}\,f\,g &= f \\
\mathsf{case}\,(\mathsf{cons}\,h\,t)\,f\,g &= g \, h \, t \\
\end{align}
$$
An encoding of this abstract type in the lambda calculus is the definition of three lambda terms $\mathsf{nil}$, $\mathsf{cons}$ and $\mathsf{case}$. Proving the correctness of this encoding means proving that the equation above holds.
Another, equivalent, definition of lists uses three destructors $\mathsf{empty}$, $\mathsf{head}$ and $\mathsf{tail}$ with the following equations (which presuppose the existence of booleans) for any terms $h$, $t$ such that $t$ is a list:
$$
\begin{align}
\mathsf{empty}\,\mathsf{nil} &= \mathsf{true} \\
\mathsf{empty}\,(\mathsf{cons}\,h\,t) &= \mathsf{false} \\
\mathsf{head}\,(\mathsf{cons}\,h\,t) &= h \\
\mathsf{tail}\,(\mathsf{cons}\,h\,t) &= t \\
\end{align}
$$
An encoding of this abstract type in the lambda calculus is the definition of five lambda terms $\mathsf{nil}$, $\mathsf{cons}$, $\mathsf{empty}$, $\mathsf{head}$ and $\mathsf{tail}$. Proving the correctness of this encoding means proving that the equation above holds.
cons
. Correctness of a function is defined relative to some function specification. There is no “absolute correctness”. Since people do not prove such trivial things, I can't guess what specification you have in mind. $\endgroup$ – beroal Jan 28 at 18:22