This is exercise 3.19 from “Type Theory and Formal Proof” by Rob Nederpelt and Herman Geuvers.
My faulty starting point: by the definition of a λ2-context we know that if Γ is a λ2-context such that L : σ is derivable from it, all free variables occurring in σ and all free variables occurring in L must be first defined in Γ. Impasse. This is trying to argue from the conclusion.
Upon reflection, I think my real problem is that I don’t know what exactly I am supposed to prove here. Is Γ a valid λ→ context and I need to show that a valid λ→ is a valid λ2 context? I think I’m assuming something that’s not there.
Or, should I assume that Γ is equivalent to some context Γ’, L : σ (for Γ’ a λ2-context) and then use induction on that? This doesn’t seem very likely, however.
I am out of ideas and would appreciate your assistance.
Thanks.
Definition 3.4.4 defines $\lambda2$-contexts. Figure 3.1 summarizes the derivation rules of $\lambda2$, i.e. when $- \vdash - : -$ holds (would have been clearer had they have written $\vdash_{\lambda2}$ instead of $\vdash$ but I guess that's a bit cluttered). So a-priori you do not know that $\Gamma \vdash L : \sigma$ only holds in cases when $\Gamma$ is a $\lambda2$-contexts. However, you can prove it by induction on the derivation of $\Gamma \vdash L : \sigma$. There are numerous examples of induction on derivations throughout the book, e.g. the proof of Lemma 2.10.3.
To address your faulty proof. You say
as if this fact is implicit in $\Gamma \vdash L : \sigma$, but it is not. Although the $\lambda2$ derivation system is designed in such a that this will be true, someone still needs to prove that. The author decided that should be you. This is to say nothing about the whole bit about the free variables on other than some vague intuition. You might find it interesting to prove later as well.