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?