[proofplan] We prove weakening simultaneously for all ordinary judgment forms by induction on the derivation of the given judgment over $\Gamma$. The context extension rule first gives the well-formed context $\Gamma,x:A$. For each non-variable inference rule, context-uniformity of the presentation says that after the induction hypothesis weakens its premises, the same rule instance may be reapplied in the extended context. The variable rule is checked separately: variables already declared in $\Gamma$ remain available after adding the fresh unused declaration $x:A$. [/proofplan] [step:Form the extended context and set up simultaneous induction] Since $\Gamma\ \mathsf{ctx}$ and $\Gamma \vdash A\ \mathsf{type}$ are derivable, and since $x$ is not declared in $\Gamma$, the context extension rule gives \begin{align*} \Gamma,x:A\ \mathsf{ctx}. \end{align*} We prove the following simultaneous statement by induction on derivations: for every ordinary raw judgment $J$ of one of the specified judgment forms, whose free variables are contained in the variables of $\Gamma$, if $\Gamma \vdash J$ is derivable, then $\Gamma,x:A \vdash J$ is derivable, provided $x$ is not free in any raw expression appearing in $J$. The induction parameter is the height of a fixed derivation $\mathcal D$ of $\Gamma \vdash J$. For each final inference rule in $\mathcal D$, we assume the weakening statement for all proper premise derivations of that rule and prove it for its conclusion. [guided] The proof is simultaneous because the inference rules of dependent [type theory](/page/Type%20Theory) do not separate cleanly by judgment form. A term-typing rule may have type-formation premises, a definitional equality rule may have typing premises, and a conversion rule may use both typing and type equality. Therefore the induction statement must cover all ordinary judgment forms at once: \begin{align*} \Gamma \vdash B\ \mathsf{type},\qquad \Gamma \vdash t:B,\qquad \Gamma \vdash B \equiv C\ \mathsf{type},\qquad \Gamma \vdash s \equiv t:B. \end{align*} The first required object is the extended context. The context extension rule applies exactly because $\Gamma$ is well formed, $A$ is a type over $\Gamma$, and $x$ is fresh for $\Gamma$. Hence \begin{align*} \Gamma,x:A\ \mathsf{ctx} \end{align*} is derivable. Now fix a derivation $\mathcal D$ of an ordinary judgment $\Gamma \vdash J$, where $J$ denotes the raw conclusion, such as $B\ \mathsf{type}$, $t:B$, $B\equiv C\ \mathsf{type}$, or $s\equiv t:B$. The freshness assumption means that $x$ occurs in none of the raw expressions appearing in $J$. We induct on the height of $\mathcal D$. The induction hypothesis says that every premise derivation occurring strictly above the last rule of $\mathcal D$ can already be weakened from $\Gamma$ to $\Gamma,x:A$. The goal is then to rebuild the last inference rule in the larger context. [/guided] [/step] [step:Reapply each non-variable inference rule by context-uniformity] Consider a final inference rule of the derivation whose conclusion is not an instance of the variable rule. Let its premises be \begin{align*} \Gamma \vdash J_1,\ldots,\Gamma \vdash J_m, \end{align*} where $m$ may be $0$, and let its conclusion be $\Gamma \vdash J$. By the induction hypothesis, for each premise $J_i$ whose derivation is proper, \begin{align*} \Gamma,x:A \vdash J_i \end{align*} is derivable. If $m=0$, context-uniformity says that the same axiom schema is available in every well-formed ambient context satisfying the same syntactic side conditions; the already established judgment $\Gamma,x:A\ \mathsf{ctx}$ supplies that ambient context. For a rule with premises, the context-uniformity hypothesis applies to the same rule instance because $x$ is fresh for the raw conclusion $J$ and, after alpha-renaming bound variables if necessary, fresh for the raw expressions occurring in the rule instance. Its side conditions are unchanged by adding the unused declaration $x:A$. Therefore the rule may be reapplied in the extended context to the weakened premises, giving \begin{align*} \Gamma,x:A \vdash J. \end{align*} [guided] We now handle every non-variable final rule at once, but this is not an extra theorem being assumed silently: it is exactly where the context-uniformity hypothesis on the chosen presentation of $\mathcal T$ is used. Suppose the last rule in the derivation has premises $\Gamma \vdash J_1,\ldots,\Gamma \vdash J_m$ and conclusion $\Gamma \vdash J$, and suppose this last rule is not the variable lookup rule. For each proper premise derivation, the induction hypothesis gives a weakened premise \begin{align*} \Gamma,x:A \vdash J_i. \end{align*} If there are no premises, the rule is an axiom schema. Context-uniformity says that such a schema is not tied to the particular context name $\Gamma$; it is available over any well-formed ambient context for which the same syntactic side conditions hold. Since the previous step proved $\Gamma,x:A\ \mathsf{ctx}$, the axiom instance is available in the extended context. If the rule has premises, context-uniformity says that adding a declaration unused by the rule instance preserves the side conditions and the raw premise and conclusion expressions. The variable $x$ is unused in the target judgment $J$ by hypothesis, and bound variables in the rule instance may be alpha-renamed before applying the rule so that no capture is introduced. Thus the same rule instance applied to the weakened premises derives \begin{align*} \Gamma,x:A \vdash J. \end{align*} This covers formation, introduction, elimination, computation, eta, congruence, reflexivity, symmetry, transitivity, conversion, and any presentation-specific non-variable rule included in $\mathcal T$, because all of them are included in the stated context-uniformity assumption. [/guided] [/step] [step:Check the variable rule in the extended context] Suppose the last rule is the variable rule. Then the conclusion has the form \begin{align*} \Gamma \vdash y:B \end{align*} for a variable $y$ declared in $\Gamma$ with type $B$ determined by its declaration and the preceding declarations in $\Gamma$. Since $x$ is not declared in $\Gamma$, the declaration of $y$ remains present in $\Gamma,x:A$. Because $x$ is not free in the raw judgment $y:B$, the type expression $B$ is unchanged by adding the unused declaration. By the named-context variable lookup convention stated in the theorem, lookup of an earlier variable is preserved after appending a later fresh declaration. Hence the variable lookup rule in the well-formed context $\Gamma,x:A$ gives \begin{align*} \Gamma,x:A \vdash y:B. \end{align*} If the variable being looked up is the last declaration $x:A$, then the conclusion would contain the variable $x$ and hence would not be one of the judgments covered by the freshness hypothesis. Thus the only variable-rule case relevant to weakening an old judgment is the old-variable case handled above. [guided] The variable rule needs a separate check because it is the one rule whose conclusion is read directly from the context. Suppose the final inference derives \begin{align*} \Gamma \vdash y:B \end{align*} by looking up a declaration of $y$ in the named context $\Gamma$. The new variable $x$ is not declared in $\Gamma$, so extending the context appends a new later declaration and does not remove or alter the earlier declaration of $y$. The theorem statement includes the standard named-context lookup convention: lookup of an earlier variable is stable under appending a later fresh declaration. Applying that convention in the well-formed context $\Gamma,x:A$ gives \begin{align*} \Gamma,x:A \vdash y:B. \end{align*} The case $y=x$ cannot occur for the old judgment being weakened, because then the raw conclusion $y:B$ would contain $x$ freely, contradicting the freshness hypothesis on $J$. [/guided] [/step] [step:Account for substituted expressions in context-uniform rule instances] The formalized statement assumes that capture-avoiding substitution is part of the raw syntax of the presentation and that, after alpha-renaming bound variables, adding a fresh unused declaration does not change substituted raw expressions appearing in a rule instance. Thus no additional substitution lemma is needed inside the induction. Whenever the final rule contains an expression obtained by substitution, that expression is the same raw expression before and after extending the ambient context by $x:A$, so the context-uniformity argument from the previous step applies unchanged. [guided] Some inference rules contain expressions produced by capture-avoiding substitution, for example a type or term obtained by replacing a bound variable by an argument. The theorem does not ask us to prove a separate substitution lemma here; instead, it builds the needed syntactic stability into the context-uniformity assumption on the presentation $\mathcal T$. Concretely, after alpha-renaming bound variables in the rule instance, the added variable $x$ is fresh for the substituted expressions occurring in that instance. The context extension therefore does not change the raw expression produced by capture-avoiding substitution. Hence every substituted premise and substituted conclusion used by the final rule is literally the same raw syntax over $\Gamma$ and over $\Gamma,x:A$. With the premises already weakened by the induction hypothesis, the same context-uniform rule instance derives the same conclusion in the extended context. [/guided] [/step] [step:Conclude the listed judgment forms as instances of simultaneous weakening] The induction covers every possible last rule in a derivation of an ordinary judgment over $\Gamma$. Therefore, for every ordinary raw judgment $J$ not containing $x$ freely, derivability of \begin{align*} \Gamma \vdash J \end{align*} implies derivability of \begin{align*} \Gamma,x:A \vdash J. \end{align*} Taking $J$ respectively to be $B\ \mathsf{type}$, $t:B$, $B\equiv C\ \mathsf{type}$, and $s\equiv t:B$ gives \begin{align*} \Gamma,x:A \vdash B\ \mathsf{type}, \end{align*} \begin{align*} \Gamma,x:A \vdash t:B, \end{align*} \begin{align*} \Gamma,x:A \vdash B \equiv C\ \mathsf{type}, \end{align*} and \begin{align*} \Gamma,x:A \vdash s \equiv t:B. \end{align*} This is precisely the weakening rule. [/step]