I am following a proof of $\forall y(Sx + y = S(x + y))$. The base case is $Sx + 0 = S(x + 0)$, and for its proof the author says this:
"If $y = 0$, note that by PA2 ($\forall x x + 0 = x$) we have $Sx + 0 = Sx = S(x + 0)"$.
Now the first equality does indeed come as a straightforward instance of PA2, but the second equivalence – $Sx = S(x + 0)$ – does not, as far as I can see. Is the author suppressing a substitution step or something here?