When $\varphi$ is a formula, $t$ is a term, and $v$ is a variable, the phrase "$t$ is free for $v$ in $\varphi$" means that for every free variable $x$ in $t$, no occurrence of $v$ in $\varphi$ is inside the scope of a quantifier binding $x$ ($\forall x$ or $\exists x$). In other words, it is "safe" to substitute $t$ for $v$ in $\varphi$, without worrying about any of the free variables in $t$ accidentally becoming bound variables. See Mauro Allegranza's answer here for a very clear explanation.
Let's look at an example of what can go wrong in your situation. Let $A(p)$ be the formula $\forall x_1\, (x_1\leq p)$. Note that $x$ is free for $p$ in $A$, but $x_1$ is not free for $p$ in $A$.
Now the sequent in question is: $$\vdash \forall p\forall x_1\,(x_1\leq x_1+p)\,\&\, x_1\leq x \supset \forall p\forall x_1\,(x_1\leq x+p)$$
This is not valid, and hence not provable.
The use of this hypothesis in the proof is hidden in the word "whence": We know $x=x_1+c$, and we have $A(x_1+c+p)$, but if $x_1$ or $x$ is bound inside $A$, they no longer refer to the same elements satisfying $x=x_1+c$. So in this case we are not justified in concluding $A(x+p)$.
Personally, I prefer to avoid this whole mess by adopting the convention that all substitutions are "capture-avoiding": that is, if a bound variable in the formula $\varphi$ also appears in the term $t$, then we swap it out for a brand new variable everywhere in $\varphi$ before substituting $t$, to avoid conflicts.
