[proofplan] We prove the admissibility of exchange by induction on the given derivation of $\Gamma,x:A,y:B,\Delta \vdash J$. The key invariant is that every judgment appearing in the derivation can be transported through the same capture-avoiding adjacent reindexing, provided its surrounding context is transformed in the corresponding way. The only non-formal part is the variable rule: variables declared before the exchange, the variables $x$ and $y$, variables declared in the tail $\Delta$, and variables declared in auxiliary local contexts introduced by rules must be checked separately. After the variable cases are established, every formation, introduction, elimination, and computation rule is reconstructed from the induction hypotheses applied to its premises. [/proofplan] [step:Define the exchange reindexing on contexts and judgments] Let $\operatorname{Init}(\Delta)$ denote the finite set of initial segments of $\Delta$. Define context-valued maps \begin{align*} C: \operatorname{Init}(\Delta) \to \{\text{raw contexts of }\mathcal T\} \end{align*} and \begin{align*} C^\sigma: \operatorname{Init}(\Delta) \to \{\text{raw contexts of }\mathcal T\} \end{align*} by \begin{align*} C(\Delta_0) := \Gamma,x:A,y:B,\Delta_0 \end{align*} and \begin{align*} C^\sigma(\Delta_0) := \Gamma,y:B,x:A,\Delta_0^\sigma. \end{align*} Here $\Delta_0^\sigma$ is obtained from $\Delta_0$ by the same recursive construction used to define $\Delta^\sigma$. Namely, if \begin{align*} \Delta_0 = z_1:C_1,\dots,z_m:C_m, \end{align*} then $\Delta_0^\sigma$ is the context \begin{align*} z_1:C_1^\sigma,\dots,z_m:C_m^\sigma, \end{align*} where each $C_i^\sigma$ is the capture-avoiding reindexing of $C_i$ from the prefix \begin{align*} \Gamma,x:A,y:B,z_1:C_1,\dots,z_{i-1}:C_{i-1} \end{align*} to the prefix \begin{align*} \Gamma,y:B,x:A,z_1:C_1^\sigma,\dots,z_{i-1}:C_{i-1}^\sigma. \end{align*} For any raw judgment $K$ over $C(\Delta_0)$, let $K^\sigma$ denote the raw judgment obtained by applying the same capture-avoiding reindexing to each displayed context entry, type, term, and definitional equality appearing in $K$. Free variables named $x$ and $y$ are not renamed; instead their declarations are read in the exchanged order. Bound variables introduced inside $K$ are alpha-renamed before reindexing if necessary, so no free variable becomes captured. If $\Theta$ is a finite local context over $C(\Delta_0)$, define $\Theta^\sigma$ recursively in the same way: the first declaration of $\Theta$ is reindexed over $C^\sigma(\Delta_0)$, and each later declaration is reindexed over the context already obtained from the previous declarations. The assumptions \begin{align*} \Gamma \vdash A\ \mathsf{type} \end{align*} and \begin{align*} \Gamma \vdash B\ \mathsf{type} \end{align*} ensure that neither $A$ nor $B$ depends on the other of the two variables being exchanged. Since $\Gamma,y:B,x:A,\Delta^\sigma\ \mathsf{ctx}$ is assumed derivable, every declaration in the reindexed tail is well formed in the context in which it is placed. [/step] [step:Prove the transported judgment by induction on the original derivation] Let $\mathcal D$ be a derivation of \begin{align*} \Gamma,x:A,y:B,\Delta \vdash J. \end{align*} We prove the following stronger assertion by induction on subderivations of $\mathcal D$. [claim:Transport invariant] For every subderivation in $\mathcal D$ whose conclusion has the form \begin{align*} C(\Delta_0),\Theta \vdash K, \end{align*} where $\Delta_0$ is an initial segment of $\Delta$ and $\Theta$ is a finite list of additional local declarations introduced inside the rule instance under consideration, the reindexed judgment \begin{align*} C^\sigma(\Delta_0),\Theta^\sigma \vdash K^\sigma \end{align*} is derivable, whenever the reindexed context \begin{align*} C^\sigma(\Delta_0),\Theta^\sigma\ \mathsf{ctx} \end{align*} is derivable. [/claim] [proof] The proof is by induction on the height of the subderivation. The induction hypothesis is applied to each premise of the last inference rule. The reindexing operation preserves the outer syntactic form of each judgment and of each rule instance: a type formation premise reindexes to a type formation premise, a term typing premise reindexes to a term typing premise, and a definitional equality premise reindexes to a definitional equality premise. It remains only to justify that the last rule can be re-applied after reindexing. For all formation, introduction, elimination, and computation rules, the stated rule-stability hypothesis on $\mathcal T$ applies: the last inference rule is schematic in the ambient context, and replacing the ambient context, displayed premises, and displayed conclusion by their capture-avoiding reindexings gives a valid instance of the same primitive rule. After applying the induction hypothesis to the displayed premises, this reindexed rule instance gives the reindexed conclusion. The variable rule requires a separate verification, carried out in the next step. Once that verification is available, every possible last inference rule is covered, and the transport invariant follows. [/proof] [guided] Let $\mathcal D$ be a derivation of \begin{align*} \Gamma,x:A,y:B,\Delta \vdash J. \end{align*} We do not prove only the final judgment at once. Instead, we prove a statement for every node of the derivation tree. This is necessary because a derivation of $J$ may contain subderivations in shorter initial contexts, or in contexts extended by temporary variables introduced by rules for dependent products, dependent sums, identity types, and other binders. The invariant is this: whenever a subderivation has conclusion \begin{align*} C(\Delta_0),\Theta \vdash K, \end{align*} where $C(\Delta_0)=\Gamma,x:A,y:B,\Delta_0$, the same derivation step can be transported to the exchanged context \begin{align*} C^\sigma(\Delta_0),\Theta^\sigma. \end{align*} The result should be \begin{align*} C^\sigma(\Delta_0),\Theta^\sigma \vdash K^\sigma. \end{align*} We prove this invariant by induction on the height of the subderivation. Suppose first that the last rule is not a variable rule. Then the rule has a finite list of displayed premises, each of which is a judgment in an appropriate local context. Applying the induction hypothesis to each premise gives the reindexed premises. The theorem statement assumes exactly the structural property needed at this point: primitive rules of $\mathcal T$ are schematic in the ambient context and stable under capture-avoiding reindexing. Therefore the original rule instance reindexes to a valid instance of the same primitive rule, and applying that rule to the reindexed premises reconstructs the reindexed conclusion. The important point is that the reindexing is capture-avoiding. If a rule introduces a bound variable, we first alpha-rename that bound variable away from $x$, $y$, and the variables already present in the surrounding context. Thus reindexing the ambient declarations does not change the binding structure of the rule instance. Consequently a lambda-introduction rule remains a lambda-introduction rule, an eliminator rule remains the same eliminator rule, and a computation rule remains the same computation rule after reindexing. The only rule whose conclusion is sensitive to the order of declarations is the variable rule. That rule is handled by splitting into cases according to whether the variable comes from $\Gamma$, is $x$, is $y$, lies in the tail $\Delta$, or lies in the auxiliary local context $\Theta$. These cases are verified explicitly below, and after they are verified the induction covers every possible last inference rule. [/guided] [/step] [step:Transport the variable rule through the exchanged context] Consider a variable judgment occurring in the original derivation. Its context has the form \begin{align*} C(\Delta_0),\Theta=\Gamma,x:A,y:B,\Delta_0,\Theta, \end{align*} where $\Delta_0$ is an initial segment of $\Delta$ and $\Theta$ is a finite auxiliary local context introduced inside the rule instance. Let the variable in the conclusion be denoted by $z$. The side condition in the transport invariant gives the well-formed exchanged context \begin{align*} C^\sigma(\Delta_0),\Theta^\sigma\ \mathsf{ctx}. \end{align*} Hence every final extension used below is a well-formed dependent context extension of the prefix from which the variable judgment is first derived. If $z$ is declared in $\Gamma$, then its type is unchanged by the exchange. Since $\Gamma$ is an initial segment of both $C(\Delta_0),\Theta$ and $C^\sigma(\Delta_0),\Theta^\sigma$, the ordinary variable rule gives the same variable judgment in $\Gamma$. The [Weakening Rule](/theorems/9622) [citetheorem:9622] transports it through the well-formed extension from $\Gamma$ to $C^\sigma(\Delta_0),\Theta^\sigma$. If $z=x$, then $x:A$ is a declaration in the swapped context prefix \begin{align*} \Gamma,y:B,x:A. \end{align*} The type $A$ is still well formed at that point because $\Gamma \vdash A\ \mathsf{type}$ is derivable and $A$ has no dependence on $y$. The variable rule gives $\Gamma,y:B,x:A \vdash x:A$, and the Weakening Rule [citetheorem:9622] transports this judgment through the well-formed extension by $\Delta_0^\sigma,\Theta^\sigma$. Hence \begin{align*} C^\sigma(\Delta_0),\Theta^\sigma \vdash x:A. \end{align*} If $z=y$, then $y:B$ is a declaration in the swapped context prefix \begin{align*} \Gamma,y:B. \end{align*} The type $B$ is well formed at that point because $\Gamma \vdash B\ \mathsf{type}$ is derivable. The variable rule gives $\Gamma,y:B \vdash y:B$, and the Weakening Rule [citetheorem:9622] transports this judgment through the well-formed extension by $x:A,\Delta_0^\sigma,\Theta^\sigma$. Hence \begin{align*} C^\sigma(\Delta_0),\Theta^\sigma \vdash y:B. \end{align*} Suppose $z$ is declared in $\Delta_0$. Write the relevant part of $\Delta_0$ as \begin{align*} \Delta_0=\Delta_1,z:C,\Delta_2. \end{align*} By definition of the swapped tail, \begin{align*} \Delta_0^\sigma=\Delta_1^\sigma,z:C^\sigma,\Delta_2^\sigma. \end{align*} Thus $z:C^\sigma$ is a declaration in the prefix $\Gamma,y:B,x:A,\Delta_1^\sigma,z:C^\sigma$. The variable rule gives the judgment for $z$ in that prefix, and the Weakening Rule [citetheorem:9622] transports it through the remaining well-formed extension $\Delta_2^\sigma,\Theta^\sigma$. Therefore \begin{align*} C^\sigma(\Delta_0),\Theta^\sigma \vdash z:C^\sigma. \end{align*} Finally suppose $z$ is declared in the auxiliary local context $\Theta$. Write the relevant part of $\Theta$ as \begin{align*} \Theta=\Theta_1,z:C,\Theta_2. \end{align*} By the recursive definition of local-context reindexing, \begin{align*} \Theta^\sigma=\Theta_1^\sigma,z:C^\sigma,\Theta_2^\sigma. \end{align*} Thus $z:C^\sigma$ is a declaration in the prefix $C^\sigma(\Delta_0),\Theta_1^\sigma,z:C^\sigma$. The variable rule gives the judgment for $z$ in that prefix, and the Weakening Rule [citetheorem:9622] transports it through the remaining well-formed extension $\Theta_2^\sigma$. Therefore \begin{align*} C^\sigma(\Delta_0),\Theta^\sigma \vdash z:C^\sigma. \end{align*} In each case, the displayed judgment is exactly the reindexing of the original variable judgment for $z$. [/step] [step:Reconstruct the final judgment in the swapped context] Apply the transport invariant to the root of the derivation $\mathcal D$. At the root, the initial segment is $\Delta_0=\Delta$ and there are no additional local declarations, so the invariant gives \begin{align*} \Gamma,y:B,x:A,\Delta^\sigma \vdash J^\sigma, \end{align*} provided \begin{align*} \Gamma,y:B,x:A,\Delta^\sigma\ \mathsf{ctx} \end{align*} is derivable. This context-validity judgment is one of the hypotheses of the theorem. Therefore the desired exchanged judgment is derivable. [/step]