[proofplan] We use the [Universal Introduction Rule](/theorems/???) with its full eigenvariable condition. Starting from the given derivation of $A(a)$, we verify both freshness requirements: $a$ is absent from every undischarged assumption and $a$ has no free occurrence in the schema $A(x)$ except the displayed occurrences being generalized. Since $a$ is free for $x$ in $A(x)$, the formula $A(a)$ is a legitimate capture-free substitution instance, and appending one universal-introduction inference yields a derivation of $\forall x\,A(x)$ from the same assumptions. [/proofplan] [step:Identify the last formula of the given derivation as a valid substitution instance] Let $\mathcal{D}$ denote the given derivation of $A(a)$ from undischarged assumptions contained in $\Gamma$. Since $a$ is free for $x$ in $A(x)$, the substitution of $a$ for the displayed free occurrences of $x$ in $A(x)$ is capture-free. Since $a$ has no free occurrence in $A(x)$ except those displayed occurrences, replacing those occurrences by $a$ is exactly the instance from which the [Universal Introduction Rule](/theorems/???) generalizes back to $\forall x\,A(x)$. Hence the final formula of $\mathcal{D}$ is exactly the substitution instance $A(a)$ to which the rule may be applied. [guided] Let $\mathcal{D}$ be the derivation supplied by the hypothesis. Its undischarged assumptions are all members of $\Gamma$, and its final formula is $A(a)$. The phrase "$a$ is free for $x$ in $A(x)$" is the syntactic condition ensuring that replacing the displayed free occurrences of $x$ by $a$ does not cause any occurrence of $a$ to become bound by a quantifier already present in $A(x)$. Therefore $A(a)$ is a legitimate capture-free substitution instance of $A(x)$. There is a second freshness point. The hypothesis that $a$ has no free occurrence in $A(x)$ except the displayed occurrences being replaced ensures that the occurrence of $a$ in $A(a)$ is only the temporary eigenvariable occurrence introduced by substitution. Without this condition, for instance with $A(x)$ equal to $(x=a)$, the inference from $a=a$ to $\forall x\,(x=a)$ would be unsound. Thus $A(a)$ is an instance to which the [Universal Introduction Rule](/theorems/???) can generalize back to the formula with $x$ universally quantified. [/guided] [/step] [step:Verify the eigenvariable condition for universal introduction] The [Universal Introduction Rule](/theorems/???) permits the inference from $A(a)$ to $\forall x\,A(x)$ provided $a$ is an eigenvariable for the inference: $a$ is not free in any undischarged assumption on which the occurrence of $A(a)$ depends, and $a$ has no free occurrence in $A(x)$ except the displayed occurrences whose substitution produced $A(a)$. By hypothesis, $a$ is not free in any undischarged assumption in $\Gamma$, and every undischarged assumption of $\mathcal{D}$ is contained in $\Gamma$. The additional freshness condition for the formula is also a hypothesis. Hence the full eigenvariable condition is satisfied for $\mathcal{D}$. [guided] The side condition on the [Universal Introduction Rule](/theorems/???) is the eigenvariable condition. For the inference from $A(a)$ to $\forall x\,A(x)$, the variable being generalized from is $a$, and two freshness requirements must be checked. First, $a$ must not occur free in any undischarged assumption on which the derived formula depends. The derivation $\mathcal{D}$ has only undischarged assumptions contained in $\Gamma$, and the theorem hypothesis states that $a$ is not free in any undischarged assumption in $\Gamma$. Therefore $a$ is not free in any undischarged assumption of $\mathcal{D}$. Second, $a$ must not already occur freely in the formula being generalized, except as the displayed occurrences substituted for $x$. This is exactly the added formula-freshness hypothesis. It rules out cases where the final formula still refers to the particular variable $a$ after $x$ is universally bound. With both requirements verified, the side condition required to infer $\forall x\,A(x)$ from $A(a)$ is satisfied. [/guided] [/step] [step:Append the universal introduction inference] Extend $\mathcal{D}$ by adding one final inference line: \begin{align*} \frac{A(a)}{\forall x\,A(x)}. \end{align*} This inference is justified by the [Universal Introduction Rule](/theorems/???), since the capture-free substitution condition and the full eigenvariable condition have both been verified. The added inference discharges no assumptions and introduces no new assumptions, so the resulting derivation has the same undischarged assumptions as $\mathcal{D}$, all contained in $\Gamma$. Therefore $\forall x\,A(x)$ is derivable from $\Gamma$. [guided] We now add one line to the end of the derivation $\mathcal{D}$. The previous final line is $A(a)$, and the new final line is obtained by universal introduction: \begin{align*} \frac{A(a)}{\forall x\,A(x)}. \end{align*} This inference is legitimate by the [Universal Introduction Rule](/theorems/???). The formula $A(a)$ is a valid capture-free substitution instance of $A(x)$; the variable $a$ is not free in any undischarged assumption of the derivation; and $a$ has no free occurrence in $A(x)$ except the displayed occurrences that were replaced to form $A(a)$. These are precisely the substitution and eigenvariable hypotheses needed for the rule. Adding this line does not add an assumption and does not discharge any assumption. Hence the extended derivation still has undischarged assumptions contained in $\Gamma$, but its final formula is now $\forall x\,A(x)$. This is precisely a derivation of $\forall x\,A(x)$ from $\Gamma$. [/guided] [/step]