Pi-calculus (or session types) - proof for weakening lemma
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.