See Wolfgang Rautenberg, A Concise Introduction to Mathematical Logic, (3rd ed - 2010).
I've a problem in "decrypting" the statement and the proof of a theorem [see page 97] :
Let $\mathcal L$ be a language and $c$ a constant symbol. $\mathcal L_c$ is the result of adjoining $c$ to $\mathcal L$.
Let $\alpha {z \over c }$ denote the formula arising from $\alpha$ by replacing $c$ with the variable $z$, and put $X {z \over c } := \{ \alpha {z \over c } | \alpha \in X \}$. $c$ then no longer occurs in $X {z \over c }$.
Lemma 2.1 (on constant elimination). Suppose $X \vdash_{\mathcal L_c} \alpha$. Then $X {z \over c } \vdash_{\mathcal L} \alpha {z \over c }$ for almost all [emphasis added] variables $z$.
Proof by rule induction in $\mathcal L_c$. If $\alpha \in X$ then $\alpha {z \over c } \in X {z \over c }$ is clear; [...].
[Consider the induction step on ($\forall_1$).] Let $\alpha, {t \over x }$ be collision-free, $X \vdash_{\mathcal L_c} \forall x \alpha$, and assume that $X {z \over c } \vdash_{\mathcal L} (\forall x \alpha) {z \over c }$ for almost all $z$. In addition, we may suppose that $z \notin var \{ \forall x \alpha, t \}$ for almost all $z$. [...]
The rules of the system are a version of natural deduction rules for $\land$ and $\lnot$ [see page 92] like :
$${X \vdash \alpha, \beta \over X \vdash \alpha \land \beta }\, \, (\land_1)$$
$${X \vdash \alpha \land \beta \over X \vdash \alpha, \beta }\, \, (\land_2)$$
and a couple of rules for the quantifier $\forall$ :
$${X \vdash \forall x \alpha \over X \vdash \alpha {t \over x } }\, \, (\alpha, {t \over x } \, \text{collision-free}) \, \, (\forall_1)$$
$${X \vdash \alpha {y \over x } \over X \vdash \forall x \alpha }\, \, (y \, \text{not free in} \, X \cup \alpha) \, \, (\forall_2)$$
plus the (Initial Rule) :
$${\over X \vdash \alpha }\, \, (\alpha \in X) \, \, \text{(IR)}$$
and the monotonicity rule :
$${X \vdash \alpha \over X' \vdash \alpha }\, \, (X \subseteq X') \, \, \text{(MR)}$$
Added
Thanks to the comment below, the above Lemma can be stated more "conventionally" as :
Suppose $X \vdash_{\mathcal L_c} \alpha$. Then $X {z \over c } \vdash_{\mathcal L} \alpha {z \over c }$ for all variables $z$, provided that $z$ is not free in $X$ nor in $\alpha$.
Due to the fact that a proof is a finite object, we can have only a finite number of free variables used in $X \vdash_{\mathcal L_c} \alpha$.
Thus, the lemma holds for "all but finitely many" variables $z$, i.e.for "almost all" variables $z$.