$ \newcommand{\abstraction}[2]{\lambda #1. #2}$ $\newcommand{\application}[2]{\left(#1 #2\right)}$ $\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$ $ \newcommand{\freevars}[1]{\operatorname{FV}\left(#1\right)}$ $\newcommand{\closedlambdaset}{\Lambda^{0}}$ $\newcommand{\lambdaexprswithfreevars}[1]{\closedlambdaset\left(#1\right)}$ $\newcommand{\subterm}[1]{\operatorname{Sub}\left(#1\right)}$ $\newcommand{\vars}[1]{\operatorname{Var}\left(#1\right)}$ $\newcommand{\context}[2]{{#1}\left[#2\right]}$ $\newcommand{\hole}{\ }$
I am trying to prove the following statement in Lambda calculus: \begin{equation} \forall \context{C}{\hole} \in \Lambda, \forall \vec{x}, \exists F \in \Lambda, \forall M \in \lambdaexprswithfreevars{\vec{x}}, \context{C}{M} = \application{F}{\left(\abstraction{\vec{x}}{M}\right)}, \end{equation} where $\context{C}{\hole}$ is a context, and $\lambdaexprswithfreevars{\vec{x}}$ is the set of all $\lambda$-expression with free variables covered by $\vec{x}$:
\begin{equation} \lambdaexprswithfreevars{\vec{x}} = \left\{ M \in \Lambda \vert \freevars{M} \subseteq \left\{\vec{x}\right\} \right\}. \end{equation}
I understand that we need to use induction to prove this lemma. However, I got stuck on the simplest case. For instance, first assume that $\context{C}{\hole} \equiv y$, a free variable, and $\vec{x}$ is an arbitrary vector of variables. Under this assumption, $\context{C}{M} = y$. Then we need to find an $F$ such that $\application{F}{\left(\abstraction{\vec{x}}{M}\right)} = y$. How should I construct such an $F$?
Next assume that $\context{C}{\hole} \equiv \context{}{\hole}$. Under this assumption, $\context{C}{M} = M$. Again, we need to construct an $F$ such that $M = \application{F}{\left(\abstraction{\vec{x}}{M}\right)}$. How should I construct this $F$?
I am attaching the definition of contexts here in case is it unclear: $x$ is a context; $\left[\ \right]$ is a context; if $\context{C_{1}}{\ }$ and $\context{C_{2}}{\ }$ are both contexts, so are $\application{\context{C_{1}}{\ }}{\context{C_{2}}{\ }}$ and $\abstraction{x}{\context{C_{1}}{\ }}$. Actually, I am curious why a single variable is thought of as a context. The original definition can be found on page 29 of "the lambda calculus: its syntax and semantics".
I don't remember ever seeing a definition of a context to include a variable. A plain variable does not have a hole, after all. But, moving on...
$F$ does not need to be well-scoped. So, for the base case where $C=y$, you can define $F$ to be $\lambda f.y$.
For the next base case, where $C[\,]=[\,]$, you can define $F$ to be the function $\lambda f. f\,\vec{x}$, where $\vec{x}$ is the $\vec{x}$ given by the statement. Then $C[M] = M$ and $F\,(\lambda\vec{x}.M) = (\lambda f. f\,\vec{x})\,(\lambda\vec{x}.M)$.
Note that in both cases, the two terms are not syntactically equal, but they are $\beta$-equivalent.