I am working through Barendregt's "The Lambda Calculus" and attempted a proof of a proposition in chapter 2 § 1.
Definitions -
$$ \begin{align} \\ \text{A $context$ C[ ]}&\text{is a term with some holes in it. More formally,} \\ &\text{$x$ is a context} \\ &\text{[ ] is a context} \\ &\text{if $C_1$[ ] and $C_2$[ ] are contexts, then so are $C_1$[ ]$C_2$[ ] and $(\lambda x.C_1$[ ]$)$} \end{align} $$
$$ \begin{align} &\text{If $C$[ ] is a context and $M \in \Lambda$, then $C$[$M$] denotes the result of placing $M$ in the holes of $C$[ ].} \\ &\text{In this act free variables of $M$ may become bound in $C$[$M$]} \end{align} $$
$$ \text{EXAMPLE: $C$[ ] $\equiv$ $\lambda x.x(\lambda y.$[ ]$)$ is a context. If $M \equiv xy$, then $C$[$M$]$\equiv\lambda x.x(\lambda y.xy)$} $$
$$ \begin{align} &\text{Contexts are not considered modulo $\alpha$-congruence.} \\ &\text{The essential feature of a context $C$[ ] is that a free variable in $M$ may become bound in $C[$M$].$} \\ &\text{$Par$ $abus$ $de$ $langage$ we write $C$[ ] $\in \Lambda$ to indicate that $C$[ ] is a context} \end{align} $$
Proposition: $\forall C[\space\space\space]\space\forall \space \vec{x} \space \exists F \space \forall M \in \Lambda^0(\vec{x})\space\space\space C[M] = F(\lambda \vec{x}.M)$
Proof: By induction on the structure of $C$[ ] (as the book hints at)
case: $C$[ ] is a variable, say $x$
then, for $F = \lambda y.x$, $F(\lambda \vec{x}.M) = x = C$[$M$]
case: $C$[ ] is [ ]
then, for $F = \lambda y.$[ ], $F(\lambda \vec{x}.M) = $ [ ] $ = C$[$M$]
case: $C$[ ] is $C_1$[ ]$C_2$[ ]
then, for $F = \lambda y.(C_1$[$y\vec{x}$]$C_2$[$y\vec{x}$]$), F(\lambda \vec{x}.M) = C$[$M$] (by induction)
case: $C$[ ] is $\lambda y.C_1$[ ]
then, for $F = \lambda z.(\lambda y.C_1$[$z\vec{x}$]$)$, $F(\lambda \vec{x}.M) = C$[$M$] (by induction)
I am happy to provide any further definitions if required