Arithmetic in intuitionistic logic In the book The Foundations of Intuitionistic Mathematis by Kleene and Vesley, one finds a proof of the following sequent:
$\vdash \forall p A(x_1+p) \& x_1 \leq x \supset \forall p A(x+p)$
where:

$p, x_1, x$ are distinct variables, and $A(p)$ is a formula in which $x_1$ and $x$ are free for $p$.

I do not understand what "$A(p)$ is a formula in which $x_1$ and $x$ are free for $p$" means and I do not see where we need such an extra condition to make the proof to work; here is the proof:

Assume $\forall p A(x_1+p) \& x_1 \leq x$. Assume $x = x_1+c$. By $\forall$-elim., $A(x_1+c+p)$, whence $A(x+p)$. By $\forall$-introd., $\forall p A(x+p)$.

 A: 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.
