In Takeuti's Proof Theory, the completeness theorem is proven only for sequents which contain no constants (or any other terms other than variables) in any of their formulas. Here is the author's definition of an "available" variable:
All the free variables which occur in any sequent which has been obtained at or before stage $k$ are said to be "available at stage $k$". In case there is none, pick any free variable and say that it is available.
It seems to me that not much is needed to extend the proof to sequents which contain other terms. In fact, it seems to me that it is enough to alter the above definiton in this way:
Let $\Gamma$ denote the set of all terms of the language which don't contain bound variables. All the elements of $\Gamma$ which occur in any sequent which has been obtained at or before stage $k$ are said to be "available at stage $k$". In case there is none, pick any element of $\Gamma$ and say that it is available.
The rules of LK listed earlier in the book aren't restricted in any way to just free variables, all of them are valid for any term. Also, it seems to me that the difference between a constant and a free variable is more-or-less a formality. I mean this in the sense that, if $P(x_1, x_2, \dots, x_n)$ is a formula with free variables $x_1, x_2, \dots, x_n$ (which are fully indicated), then it is valid in all models and all their interpretations if and only if the formula $P(c_1, c_2, \dots, c_n)$, where the $c_1, c_2, \dots, c_n$ are constants, is valid in all models and all their interpretations.
What confuses me here is why the author skipped over this. It really doesn't complicate the proof much at all and formulas which include constant terms are obviously a pretty important part of any language. Is my reasoning somehow wrong? Is the construction of a reduction tree significantly harder if we don't ignore the formulas which contain constant terms?