How to Prove a Lemma in Lambda Calculus about Contexts $ \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".
 A: 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.
A: $\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've been trying to prove the same theorem for a few days now: lemma 2.1.20(i) of Barendregt's The Lambda Calculus, Its Syntax and Semantics. The answer by fragala in this thread helped me advance as I was stuck trying to define a single $F$ for all 4 cases. So I went like so:
I want $F\left(\abstraction{\vec{x}}{M}\right) = C[M]$.
Abstracting $M$ on the rhs:
$F \left(\abstraction{\vec{x}}{M}\right) = \left(\abstraction{g}{\context{C}{\application {g}{\vec{x}}}}\right) \left(\abstraction{\vec{x}}{M}\right)$
Resulting in the choice of $F = \abstraction{g}{\context{C}{\application {g}{\vec{x}}}}$
By induction on the structure of the context.

*

*Case 1: $\context{C}{} = a$ and $\context{C}{M} = a$.
Then $F = \abstraction{g}{a}$ and $F \left(\abstraction{\vec{x}}{M}\right) = \left( \abstraction{g}{a} \right) \left(\abstraction{\vec{x}}{M}\right) = a = \context{C}{M}$


*Case 2. $\context{C}{} = \context{}{}$ and $\context{C}{M} = M$.
Then $F = \abstraction{g}{\application{g}{\vec{x}}}$ and $F \left(\abstraction{\vec{x}}{M}\right) = \left( \abstraction{g}{\application{g}{\vec{x}}} \right) \left(\abstraction{\vec{x}}{M}\right) = \left(\abstraction{\vec{x}}{M}\right) \vec{x} = M = \context{C}{M}$
Note that the above are equivalent to frabala's.

*

*Case 3. $\context{C}{} = \abstraction{y}{\context{C_1}{}}$ and $\context{c}{M} = \abstraction{y}{\context{C_1}{M}}$ such that $\context{C_1}{M} = F \left( \abstraction{\vec{x}}{M} \right)$ as per the induction hypothesis.
Then $F \left( \abstraction{\vec{x}}{M} \right) = 
\left( \abstraction{g}{\abstraction{y}{\context{C_1}{\application{g}{\vec{x}}}}} \right) \left( \abstraction{\vec{x}}{M} \right) = 
\abstraction{y}{\context{C_1}{\left( \abstraction{\vec{x}}{M} \right) \vec{x}}} = 
\abstraction{y}{\context{C_1}{M}} = \context{C}{M}$


*Case 4. $\context{C}{} = \application{\context{C_1}{}}{\context{C_2}{}}$ and $\context{C}{M} = \application{\context{C_1}{M}}{\context{C_2}{M}}$ such  that $\context{C_1}{M} = F_1 \left( \abstraction{\vec{x}}{M} \right)$ and $\context{C_2}{M} = F_2 \left( \abstraction{\vec{x}}{M} \right)$ per the induction hypothesis.
Then $F \left( \abstraction{\vec{x}}{M} \right) = \left(\abstraction{g}{\application{\context{C_1}{\application{g}{\vec{x}}}}{\context{C_2}{\application{g}{\vec{x}}}}}\right)\left( \abstraction{\vec{x}}{M} \right) = 
\application{\context{C_1}{M}}{\context{C_2}{M}} = \context{C}{M}$
What annoys me is that I didn't need the induction hypothesis in cases 3 and 4.
