The version of Buss's proof I'm referring to is the proof of Lemma II.2.24 in Logical Foundations of Proof Complexity by Cook and Nguyen. In the interest of keeping this question self-contained I've provided all the particularities of the book in the "Notations, Conventions and Definitions" section at the end of this question.
Background
Theorem II.2.23: Let $\mathcal{L}$ be a first-order language which does not contain the equality symbol. Let $\Phi$ be a set of formulas of $\mathcal{L}$, and $\Gamma \rightarrow \Delta$ be a sequent of $\mathcal{L}$. There is an LK-$\Phi$ proof of $\Gamma \rightarrow \Delta$ iff $\forall \Phi \vDash \Gamma \rightarrow \Delta$.
The proof of this theorem relies on the following Lemma.
Lemma II.2.24: If $\Phi \vDash \Gamma \rightarrow \Delta$, then there is a cut-free LK proof of $C_1, C_2, ..., C_k, \Gamma \rightarrow \Delta$, where $\{C_i : i \in [k]\}$ is a finite subset of $\Phi$.
My question pertains specifically to the proof of completeness.
Proof of completeness direction of Theorem II.2.23: Let $\Phi$ be a set of formulas such that $\forall \Phi \vDash \Gamma \rightarrow \Delta$. By Lemma II.2.24, we know there is finite subset ${C_1,...,C_k}$ of $\Phi$ such that there is an LK proof $\pi$ of $S := \forall C_1, ..., \forall C_k, \Gamma \rightarrow \Delta$. Notice that if we can derive, for any $i \in [k]$, the sequent $\rightarrow \forall C_i$, then we are done: by weakening each such sequent appropriately, we can apply the cut rule to remove $\forall C_i$ from $S$. Applying all such cuts yields an LK-$\Phi$ proof $\pi'$ of the sequent $\Gamma \rightarrow \Delta$.
It remains to show that we can derive $\forall C_i$. Starting from nonlogical axiom $\rightarrow C_i$, we can apply the right $\forall$-introduction rule for each free variable in $C_i$. $\blacksquare$
Note that in $\pi'$ above, we cut on formulas of the form $\forall C_i$. Since $\pi'$ is an LK-$\Phi$ proof and not an LK-$\forall \Phi$ proof, this means that $\pi'$ is not necessarily anchored. However according to the book (assuming certain conditions on $\Phi$), it is possible to show that an anchored LK-$\Phi$ proof of $\Gamma \rightarrow \Delta$ exists. In the book, this is Theorem II.2.28. Proving this theorem is Exercise II.2.29.
My Question
How isn't the following simple modification to the proof above a proof of anchored derivational completeness of LK?
(Proposed) Proof: Let $\Phi$ be a set of $\mathcal{L}$-formulas such that $\forall \Phi \vDash S$, where $S := \Gamma \rightarrow \Delta$. By Lemma II.2.24, we know there is finite subset ${C_1,...,C_k}$ of $\Phi$ such that there is a cut-free LK proof $\pi$ of $S := C_1, ..., C_k, \Gamma \rightarrow \Delta$. For any $i \in [k]$, by weakening each nonlogical axiom $\rightarrow C_i$ appropriately, we can apply the cut rule to remove $C_i$ from $S$. Applying all such cuts yields an LK-$\Phi$ proof $\pi''$ of the sequent $\Gamma \rightarrow \Delta$.
Since the only cuts in $\pi''$ are on $C_i \in \Phi$, we conclude $\pi''$ is an anchored LK-$\Phi$ proof of $\Gamma \rightarrow \Delta$. $\blacksquare$
Notations, Conventions and Definitions
Let $\mathcal{L}$ be a first order language. We define two disjoint, infinite set of variables of $\mathcal{L}$: free variables, and bound variables. As a convention, in any formula $A$ of $\mathcal{L}$ we require that there are no bound occurrences of free variables and that there are no free occurrences of bound variables in $A$.
We say formula $B$ is a logical consequence of $A$, denoted $A \vDash B$, if for every $\mathcal{L}$-structure $\mathcal{M}$ and every object assignment $\sigma$ from the variables of $L$ to the universe $M$ of $\mathcal{M}$, if $\mathcal{M}$ satisfies $A$ under $\sigma$, denoted $\mathcal{M} \vDash A[\sigma]$, then $\mathcal{M} \vDash B[\sigma]$.
If $\Phi$ is a set of formulas $\{A_i\}$, then we say $\mathcal{M}$ satisfies $\Phi$ under $\sigma$, denoted $\mathcal{M} \vDash \Phi[\sigma]$, if $\mathcal{M} \vDash A_i[\sigma]$ for all $i$. We say $B$ is a logical consequence of $\Phi$, denoted $\Phi \vDash B$, if $\mathcal{M} \vDash \Phi[\sigma]$ implies $\mathcal{M} \vDash B[\sigma]$.
Let $S := \Gamma \rightarrow \Delta$ be a sequent where $\Gamma := \{A_1, ..., A_m\}$ and $\Delta := \{B_1, ..., B_n\}$ are sets of $\mathcal{L}$-formulas. We define $A_S$ as the first order formula
$$\lnot A_1 \lor \lnot A_2 \lor ... \lor \lnot A_m \lor B_1 \lor B_2 \lor ... \lor B_n$$
and we say that $\mathcal{M}$ satsifies $S$ under $\sigma$, denoted $\mathcal{M} \vDash S[\sigma]$, if $\mathcal{M} \vDash A_S[\sigma]$. We say $S$ is a logical consequence of $\Phi$, denoted $\Phi \vDash S$, if $\mathcal{M} \vDash \Phi[\sigma]$ implies $\mathcal{M} \vDash S[\sigma]$.
An LK proof of $S$ is a tree $\pi$ with root is $S$ whose leaves are sequents $A \rightarrow A$ for any formula $A$, $\bot \rightarrow$, or $\rightarrow \top$ (we call these sequents logical axioms) and whose internal nodes are sequents such that if node $S'$ has set of children $H$, then $H$ is the set of hypothesis (top) sequents and $S'$ is the conclusion (bottom) sequent of one of the following rules.
where $A(t)$ is the formula obtained by replacing all free occurrences of $x$ in $A(x)$ (i.e. the occurrences of $x$ in $\forall x A(x)$ which become free when we remove the $\forall x$ quantifier), with a term $t$ consisting entirely of free variables. Similarly, $A(b)$ is the formula obtained by replacing all free occurrences of $x$ in $A(x)$ by free variable $b$. In the left $\exists$-introduction and right $\forall$-introduction rules, $b$ must not occur anywhere in the conclusion sequent.
An LK-$\Phi$ proof of $S$ is an LK proof of $S$ in which we allow the leaves to be sequents of the form $\rightarrow A_i$ for $A_i \in \Phi$, which we call nonlogical axioms, in addition to the logical axioms.
We say that an LK-$\Phi$ proof is cut-free if it does not use the cut rule, and we say that it is anchored if the only formulas it cuts appear in $\Phi$.
Note that two rules of $LK$ aren't "sound" in the sense that the conclusion sequent is not a logical consequence of the hypothesis sequent: right $\forall$-introduction and left $\exists$-introduction. As such, it is necessary to tweak the usual definition of soundness a bit in order to speak of the soundness of LK. We do this with the universal closure.
The universal closure of $A$, denoted $\forall A$, is the formula $\forall x_1 ... \forall x_k A$, where $x_1, ..., x_k$ are all the free variables of $A$. We define the universal closure of $\Phi$, denoted $\forall \Phi$, as $\{\forall A_i\}$.
