Well said. I completely disagreed with you until half-way through the second paragraph. In Physics it is very common to see the versions of a theorem made simpler by substituting constants for variables. But you are specifically talking about "free variables" and that reminded me of some of the fields that come up in the GR generalizations of inner product spaces. The induced fields only have the properties of satisfying the local boundary conditions. You could never replace those with any kind of scalars imaginable.The idea is whether we can take a derivation and systematically replace all free occurrences of a certain variable by a constant or vice versa. The beginning of the paragraph before the underlined text points out that only variables can be generalized by (∀I). That is, if we have a formula A(x) containing x free (and x does not occur free in open assumptions), then we can derive ∀x A(x). However, if we replace x with c everywhere in the derivation and, in particular, in A(x), we can no longer apply (∀I). Therefore, a constant cannot in general take the place of a variable in a derivation.
Why a constant can be replaced with a variable is best understood by trying to prove Theorem 2.8.3(i), which I recommend doing very explicitly and carefully. Propositional rules do not depend on whether formulas involved contain variables or constants. This means that the inductive step for such rules follows directly from the inductive hypotheses (and the fact that substitutions commute with propositional connectives). The step for (∀E) uses the fact that $A[s/x][t/y]=A[t/y][s[t/y]/x]$ (where exactly?). However, the case of (∀I) turned out to be trickier than I first thought. I need to consult the book for the details of the definition of (∀I). It is also interesting that the theorem assumption says that $x$ does not occur in $\varphi$ at all instead of occur free. I invite you to try the proof and write your thoughts on whether induction does or does not go through for (∀I). I'll try to post my thoughts tomorrow.