Fresh constants may be eliminated from a finite proof

The finite proof and its finitely many finite annotations mention only finitely many variables. Choose the least-index variable $z$ not mentioned. Replace every token $c$ in formulas and substitution data by $z$, leaving binders unchanged. No binder is $z$, so every inserted $z$ remains free. Assumption lines are unchanged since $c$ is absent from $T$.

A Boolean axiom remains the same tautology pattern with transformed substituted formulas; reflexivity remains reflexivity. For either quantifier substitution axiom and the equality substitution axiom, token replacement commutes with the indicated free-variable substitution. Its new term can gain only the free variable $z$, and no binder in the transformed matrix is $z$, so every former free-for condition still holds. Universal distribution's restricted variable is an old variable: replacing $c$ by $z$ creates no free occurrence of that old variable in its antecedent. Thus every transformed axiom is an axiom of the smaller signature.

MP retains the identical implication/premise matching. A generalization in an old variable still generalizes that variable after replacement. For existential elimination the eliminated variable is old and distinct from $z$; the consequent gains no occurrence of it, so its restriction persists. Therefore induction along the unchanged reference indices gives a valid transformed derivation. Generalization in $z$ may be appended because the base assumptions are sentences.

If the conclusion omits $c$, it is unchanged by this operation; we obtain the asserted smaller-language proof. A proof in an expansion by any set of fresh constants mentions only finitely many of them. Remove them one at a time by the operation above, each time taking a new variable outside the finite current proof. The final proof uses only the original signature. Conversely every original proof is still a proof in the expansion. Hence the expansion is conservative.