Stuck in this Proof of the Completeness Theorem for Predicate Logic

I'm studying a proof of the completeness theorem for predicate logic shown in this lecture and I'm caught in an obstacle. It proceeds by showing that if a theory is consistent, then it has a model, and my problem specifically points at a lemma, namely the part where it proves that the theory $$T'$$ is consistent. I should name a definition..

Definition 11.2$$\hspace{0.2in}$$A henkin theory is a theory $$T$$ so that for every formula $$\phi$$ and variable $$x,$$ there is a constant symbol $$c$$ such that $$(\exists x\phi\rightarrow\phi^x_c)\in T.$$

and we have that lemma..

Lemma 11.3$$\hspace{0.2in}$$Suppose that $$L$$ is a language and $$T$$ is a consistent theory in $$L,$$ then there is a language $$L'\supseteq L$$ obtained by adding constant symbols to $$L$$ and a theory $$T''\supseteq T$$ that is consistent, syntactically complete, and is a henkin theory.

It begins the proof by defining a sequence of languages and theories $$L_0,L_1,...$$ and $$T_0,T_1,...$$ such that $$L_0=L,$$ $$T_0=T,$$ and $$L_{n+1}$$ defined by adding to the language $$L_n$$ all constant symbols $$c_{\exists x\phi}$$ for every formula $$\exists x\phi$$ in $$L_n,$$ with $$T_{n+1}$$ defined by adding to $$T_n$$ all formulas $$(\exists x\phi\rightarrow\phi^x_{c_{\exists x\phi}})$$ for every formula $$\phi$$ in $$L_n.$$ $$L'$$ and $$T'$$ are defined to be the union of all languages $$L_0,L_1,...$$ and all theories $$T_0,T_1,...$$ respectively. It follows that $$T'$$ is a henkin theory by assuming that if $$\phi$$ is a formula in $$L',$$ then $$\phi\in L_n$$ for some number $$n,$$ from which by definition, $$(\exists x\phi\rightarrow\phi^x_{c_{\exists x\phi}})\in T_{n+1}\subseteq T'.$$

Then it proceeds to prove that $$T'$$ is a consistent theory. It's easy to tell that it suffices to prove that all theories $$T_n$$ for each $$n$$ is consistent, hence we proceed by proof by induction on the said sequence of theories. For the basis, $$T_0=T$$ which is by definition, consistent. For the induction step, we assume that $$T_n$$ is consistent and by way of contradiction, that $$T_{n+1}$$ is inconsistent. The proof further goes as follows (I shall mark the questionable part with "???"):

Then since $$T_{n+1}$$ is obtained from $$T_n$$ by adding formulas of the form $$(\exists x\phi\rightarrow\phi^x_{c_{\exists x\phi}}),$$ there must be some finite number of such formulas $$\phi_1,...,\phi_k$$ such that $$T_n\cup\{(\exists x\phi_i\rightarrow(\phi_i)^x_{c_{\exists x\phi_i}}):i\le k\}$$ is inconsistent. Then using proof by contradiction, $$T_n\cup\{(\exists x\phi_i\rightarrow(\phi_i)^x_{c_{\exists x\phi_i}}):i\le k-1\}\vdash\neg(\exists x\phi_k\rightarrow(\phi_k)^x_{c_{\exists x\phi_k}}).$$ Let $$Q=T_n\cup\{(\exists x\phi_i\rightarrow(\phi_i)^x_{c_{\exists x\phi_i}}):i\le k-1\}$$ then since $$(\neg(p\rightarrow q)\rightarrow p)$$ and $$(\neg(p\rightarrow q)\rightarrow\neg q)$$ are tautologies, we have that $$Q\vdash\exists x\phi_k$$ and $$Q\vdash\neg(\phi_k)^x_{c_{\exists x\phi_k}},$$ but then by generalization on constant applied to this last fact, we see that $$Q\vdash\forall x\neg\phi_k (???),$$ hence $$Q\vdash\neg\exists x\phi_k,$$ so $$Q$$ is inconsistent. Proceeding this way, we can eliminate all the formulas $$(\exists x\phi\rightarrow(\phi_i)^x_{c_{\exists x\phi_i}})$$ for all $$i=k,...,1$$ and show that $$T_n$$ itself is inconsistent, which is a contradiction.

Here, it seems that the author uses the stronger universal generalization rule (which is applicable to terms as long as that choice of terms remains arbitrary), whereas I'm working in classical predicate logic with only the generalization metatheorem (which is applicable only to variables) stated as follows (from Enderton's book, "A Mathematical Introduction to Logic"):

If $$\Gamma\vdash\varphi$$ and $$x$$ does not occur free in any formula of $$\Gamma,$$ then $$\Gamma\vdash\forall x\varphi.$$

Here I assume that $$x$$ is a variable because it either should not occur at all or occurs bound (and constant symbols which are non-variable terms don't "occur bound").

So far, all I've been trying to do is finding a proof for the "stronger" generalization metatheorem or an alternative way to prove that $$Q$$ is inconsistent but to no avail. Your help will be very much appreciated.

• See Enderton, page 123 : THEOREM 24F (GENERALIZATION ON CONSTANTS) Assume that $\Gamma \vdash ϕ$ and that $c$ is a constant symbol that does not occur in $\Gamma$. Then there is a variable $y$ (which does not occur in $ϕ$) such that $\Gamma \vdash ∀y ϕ^c_y$. – Mauro ALLEGRANZA May 15 at 6:14
• "is applicable only to variables" : where would the idea differ ? A constant is just a fancy variable. Of course this is not precise, but if you look at the proof for variables, and change the word "variable" to "constant" surely it applies as well. Think about it : if you can proof $\phi(c)$ with no hypotheses on $c$ ($c$ a constant); then surely you can prove $\phi(y)$ for any variable $y$ not having been used in the proof, and so by generalization $\forall y, \phi(y)$ – Max May 15 at 11:23