I would like to understand a step in this (incomplete) gentzen-style natural deduction tree. For the $\forall I$ step it must hold that $y$ is not free in $\forall x.p(x)$. I don't understand why this holds. Obviously $x$ is not free in $\forall x.p(x)$ because $\forall x$ binds $x$, but $\forall x$ doesn't bind $y$, so $y$ could be free in $\forall x.p(x)$, or?
The rules are:
with the $\text { Side condition } *: x \text { not free in any assumption in } \Gamma$