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&#39;$."

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

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?
I still think there is an imprecision in how he uses the lemma. However there is a solution (I must thank to Barbara Petit who came with the solution).

In fact, the solution comes from the definition of $\geq$ (def. 4.2.1), which is morally this:

$\sigma&gt;\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&gt;\forall\alpha.\sigma$, then $\alpha\notin FV(\Gamma)$, which is exactly what he needs in the proof (and from where the imprecision comes).