I'm writing a thesis about session types and am currently writing a section concerning type soundness for the system. I started to proof weakening lemma, which states, that $$ \text{If } \Gamma \vdash P, \text{ then } \Gamma, x:T \vdash P. $$ That is, names not free in a process can be added to the typing environment. However, I can't understand how to find a derivation for $$ \Gamma, x:T \vdash (\upsilon x)P $$ The rule T-RES for restriction is $$ \frac { \Gamma, x:T \vdash P } { \Gamma \vdash (\upsilon x)P } $$ I tried to find a proof for the lemma (for session types, pi-calculus or other calculi), but all the proofs seemed to be something like "a straightforward induction on the derivation of $\Gamma \vdash P$".
I'm trying to understand, what I'm misunderstanding or missing. The rule T-PAR explicitly states, that $x$ is not in the environment in $\Gamma \vdash (\upsilon x)P$. However, the lemma states, that $\Gamma, x:T \vdash (\upsilon x)P$ is valid.