The Lemma on Constants is an elementary result, which says something like the following:
Lemma: Suppose T ⊢ ϕ(c), where T is a theory, ϕ(x) is a formula, x is a tuple of variables, and c is a tuple of constant symbols not appearing in T. Then T ⊢ ∀x : ϕ(x).
Proof: If one interprets T ⊢ ψ to mean that ψ holds in all models of T, then this follows from unwinding the definitions: T ⊢ ϕ(c) means that whenever M is a model of T and c is a tuple from M, M ⊨ ϕ(c). Then clearly M ⊨ ∀x : ϕ(x)!
On the other hand, if one interprets T ⊢ ψ to mean that ψ can be proven from T, then this follows from the other version by Gödel's Completeness Theorem, which says that these two interpretations of ⊢ are the same. QED.
The Lemma on Constants is practically obvious. However, it is handy to have a name for this lemma when making technical arguments. ::: ::: :::