# Barendregt's proof of subject reduction for $\lambda2$

I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types).

The last step of the proof (page 60), says:

"and hence by Lemma 4.1.19(1), $\quad\Gamma,x:\rho\vdash P:\sigma'$."

However, according to Lemma 4.1.19(1) it should be $\Gamma[\vec{\alpha}:=\vec{\tau}],x:\rho\vdash P:\sigma'$, since the substitution is made to the whole context, not only to $x:\rho'$.

I guess the standard solution may be to somehow prove that $\vec{\alpha}\notin FV(\Gamma)$, but I am not sure how.

I had a proof simplifying it by relaxing the generation lemma of abstractions, but I recently found that there was a mistake and my proof is wrong, so I am not sure how to solve this problem any more.

Can somebody, please, tell me what I am missing here?

• Barendregt assumes the so-called variable convention, that bound variable names and free variable names are standardized apart, namely, we implicitly assume that they are different (using $\alpha$-conversion. Maybe this helps. Nov 9, 2011 at 14:31
• Thanks for your answer. But yet, it does not solve the problem. He arrives to $\Gamma,x:\rho\vdash P:\sigma'$ by using Lemma 4.1.19(1) in the following way: we has $\Gamma,x:\rho'\vdash P:\sigma''$ and we knows that $\rho'[\vec{\alpha}:=\vec{\tau}]=\rho$ and $\sigma''[\vec{\alpha}:=\vec{\tau}]=\sigma'$, so using that lemma, he can do the same substitution in the context and the inferred type at the same time... but he only substitutes on the x:\rho', no all the context! And that is my problem... Nov 9, 2011 at 15:03

In fact, the solution comes from the definition of $\geq$ (def. 4.2.1), which is morally this:
$\sigma>\rho\quad$ if $\quad\dfrac{\Gamma\vdash P:\sigma}{\Gamma\vdash P:\rho}$
However, instead of defining it in that way, he defines the relation in terms of the types only. The advantage on defining it in terms of sequents, is that we can deduce that if $\sigma>\forall\alpha.\sigma$, then $\alpha\notin FV(\Gamma)$, which is exactly what he needs in the proof (and from where the imprecision comes).