# Pi-calculus (or session types) - proof for weakening lemma

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.

You should $$\alpha$$-rename to avoid conflict with the variable names. That is, you should prove weakening of the form: $$\Gamma \vdash (\upsilon y) P$$ implies $$\Gamma, x : T \vdash (\upsilon y) P$$.
$$\alpha$$-equivalence and capture-avoiding substitution is an important concept to understand in type theory: I would recommend studying this concept for the untyped or simply-typed $$\lambda$$-calculus to begin with, before trying to prove things about a more complicated calculus.