[proofplan] We first separate judgment bodies from complete judgments, so that substitution acts on the body while the ambient context changes. The main argument is a simultaneous induction on derivations of all five judgment forms, proving the general substitution theorem for every well-typed context morphism. Weakening and dependency-respecting exchange are then special cases of substitution, using respectively the projection from an extended telescope and the context isomorphism induced by the dependency-respecting permutation. The conversion clauses follow from the primitive conversion rule, or from the explicitly assumed invariance of typing and equality under definitionally equal types. [/proofplan] [step:Formulate the simultaneous substitution property for all judgment forms] Let $\mathsf{Jud}$ denote the collection of the five judgment forms displayed in the statement. For a non-context judgment body $J$ over a context $\Gamma$, write $\Gamma\vdash J$ for the corresponding complete judgment. For the context judgment, regard the assertion $\Gamma\ \mathsf{ctx}$ as the context-validity component of the same simultaneous induction, not as a judgment body to which another ambient context is attached. We prove the following property $P(\mathcal D)$ for every derivation $\mathcal D$ in $\mathcal T$: whenever $\mathcal D$ derives one of the five judgment forms, substitution along any well-typed context morphism preserves that derivation. More explicitly, if $\mathcal D$ derives $\Gamma\ \mathsf{ctx}$ and $\sigma:\Delta\to\Gamma$ is a context morphism, then $\Delta\ \mathsf{ctx}$ is already part of the data of $\sigma$. If $\mathcal D$ derives a non-context judgment $\Gamma\vdash J$ and $\sigma:\Delta\to\Gamma$ is a context morphism, then $P(\mathcal D)$ asserts that \begin{align*} \Delta\vdash J[\sigma] \end{align*} is derivable. [guided] The statement uses the compact notation $\Gamma\vdash J$, but this notation should be read carefully. For a type judgment, $J$ may be the body $A\ \mathsf{type}$; for a term judgment, $J$ may be the body $a:A$; for type equality, $J$ may be the body $A\equiv B\ \mathsf{type}$; and for term equality, $J$ may be the body $a\equiv b:A$. Thus substitution changes the body $J$ and also changes the ambient context from $\Gamma$ to $\Delta$. The context judgment $\Gamma\ \mathsf{ctx}$ is different: it is already a complete judgment and is not written as an assertion inside a larger context. We therefore include context formation as a separate component in the simultaneous induction. This is necessary because rules for type formation, term typing, and definitional equality all refer back to well-formedness of contexts. The property to be proved is the following uniform substitution property. Let $\mathcal D$ be a derivation of a non-context judgment $\Gamma\vdash J$. Let \begin{align*} \sigma:\Delta\to\Gamma \end{align*} be a context morphism, meaning a well-typed simultaneous substitution from $\Delta$ into $\Gamma$. Then the substituted judgment \begin{align*} \Delta\vdash J[\sigma] \end{align*} must be derivable. For example, if $J$ is $a:A$, then $J[\sigma]$ is $a[\sigma]:A[\sigma]$; if $J$ is $A\equiv B\ \mathsf{type}$, then $J[\sigma]$ is $A[\sigma]\equiv B[\sigma]\ \mathsf{type}$. The context case says no more than what the definition of context morphism already contains: a morphism $\sigma:\Delta\to\Gamma$ has a well-formed source context $\Delta$ and a well-formed target context $\Gamma$. Thus the context-validity component supplies the base needed for the other four judgment forms. [/guided] [/step] [step:Prove substitution by induction on the last inference rule] We prove $P(\mathcal D)$ by induction on the height of $\mathcal D$, simultaneously over context formation, type formation, term typing, type equality, and term equality. Suppose first that $\mathcal D$ ends with a primitive inference rule $R$. Let the premises of $R$ be derivations $\mathcal D_1,\ldots,\mathcal D_m$, and let the conclusion be $\Gamma\vdash J$. Let $\sigma:\Delta\to\Gamma$ be a context morphism. By the induction hypothesis applied to $\mathcal D_1,\ldots,\mathcal D_m$, each substituted premise of $R$ along $\sigma$ is derivable in $\Delta$. Since the primitive rules of $\mathcal T$ are assumed to be stable under the displayed substitution action, the substituted instance of $R$ has exactly these substituted premises and conclusion \begin{align*} \Delta\vdash J[\sigma]. \end{align*} Applying this substituted instance of $R$ gives the desired derivation. If the final inference uses alpha-renaming of bound variables, the assumed stability under alpha-renaming identifies the renamed rule instance with the corresponding schematic instance before applying the same argument. If the final inference uses a definitional-equality congruence rule, the same induction applies to its premises, and the assumed typed congruence of definitional equality reconstructs the substituted equality judgment. [guided] We now prove the core theorem: substitution preserves derivability. The proof is by induction on derivations, and it must be simultaneous because the inference rules for one judgment form mention the others. For instance, a term-introduction rule may require a type-formation premise; a definitional-equality rule may require typing premises; and a context-extension rule requires both context validity and type formation. Fix a derivation $\mathcal D$ whose conclusion is a non-context judgment \begin{align*} \Gamma\vdash J. \end{align*} Fix also a context morphism \begin{align*} \sigma:\Delta\to\Gamma. \end{align*} We must construct a derivation of \begin{align*} \Delta\vdash J[\sigma]. \end{align*} Inspect the last inference rule used in $\mathcal D$. Suppose it is a primitive rule $R$ with premise derivations $\mathcal D_1,\ldots,\mathcal D_m$. Each premise is itself one of the same judgment forms, possibly in a context built from $\Gamma$. By the induction hypothesis, substituting along $\sigma$ sends each premise derivation to a valid substituted premise derivation over $\Delta$. Now we use exactly the structural hypothesis on the presentation $\mathcal T$. The primitive rules are not merely written for particular variable names; they are schematic in variables and stable under simultaneous capture-avoiding substitution. Therefore, after replacing every premise and the conclusion of $R$ by its image under $\sigma$, we again have a legitimate instance of the same primitive rule. Its premises are precisely the substituted premises already obtained by the induction hypothesis, and its conclusion is \begin{align*} \Delta\vdash J[\sigma]. \end{align*} Applying this substituted rule instance completes the inductive step. Alpha-renaming causes no separate difficulty. If the last rule was applied after changing bound variable names, the assumed stability under alpha-renaming allows us to choose fresh representatives before substitution and then identify the result with the capture-avoiding substituted judgment. This is the point of insisting on capture-avoiding substitution rather than naive textual replacement. Finally, if the last rule is a congruence or equality rule for definitional equality, the induction hypothesis gives the substituted typing and equality premises. The assumption that definitional equality is a typed congruence compatible with type equality then gives the substituted equality conclusion in the correct type. Thus all primitive rule cases, including formation, introduction, elimination, computation, and congruence rules for the type formers of $\mathcal T$, are covered by the same induction. [/guided] [/step] [step:Deduce weakening from substitution along the projection] Let $\Gamma,\Xi$ be a well-formed telescope extension of $\Gamma$. Define the projection context morphism \begin{align*} \rho:\Gamma,\Xi\to\Gamma \end{align*} to be the sequence sending each declaration $x_i:A_i$ of $\Gamma$ to the corresponding variable $x_i$ in the extended context $\Gamma,\Xi$. The variable rule and the well-formedness of $\Gamma,\Xi$ give the required typing premises for this sequence, so $\rho$ is a context morphism. If $\Gamma\vdash J$ is derivable, the substitution theorem applied to $\rho$ gives \begin{align*} \Gamma,\Xi\vdash J[\rho]. \end{align*} This is precisely the admissible [weakening rule](/theorems/9622). [/step] [step:Deduce exchange from substitution along the induced context isomorphism] Let $\pi$ be a permutation of the declarations of $\Gamma$ such that $\pi\Gamma$ is a well-formed telescope and such that $\pi$ induces the context isomorphism \begin{align*} \pi:\pi\Gamma\to\Gamma. \end{align*} Because $\pi$ is assumed dependency-respecting, each declaration of $\Gamma$ is assigned the corresponding variable in $\pi\Gamma$ with all dependencies already available in the permuted telescope. Hence the variable rule supplies the typing premises required for $\pi$ to be a context morphism. Given a derivation of $\Gamma\vdash J$, applying the substitution theorem to the context morphism $\pi:\pi\Gamma\to\Gamma$ yields \begin{align*} \pi\Gamma\vdash J[\pi]. \end{align*} This is exactly the admissible dependency-respecting exchange rule. The argument uses only permutations that produce a well-formed telescope and a genuine context isomorphism, so no arbitrary exchange of dependent declarations is being asserted. [/step] [step:Obtain conversion from the conversion hypothesis] Assume first that $\mathcal T$ has the usual conversion rule as a primitive rule. Then from derivations of \begin{align*} \Gamma\vdash a:A \end{align*} and \begin{align*} \Gamma\vdash A\equiv B\ \mathsf{type} \end{align*} the primitive conversion rule gives \begin{align*} \Gamma\vdash a:B. \end{align*} Similarly, from \begin{align*} \Gamma\vdash a\equiv b:A \end{align*} and \begin{align*} \Gamma\vdash A\equiv B\ \mathsf{type} \end{align*} the equality-conversion form gives \begin{align*} \Gamma\vdash a\equiv b:B. \end{align*} If instead conversion is not primitive, the statement assumes that typing and equality judgments are invariant under replacing a type by a definitionally equal type in the same context. Applying that invariance to the displayed type equality $\Gamma\vdash A\equiv B\ \mathsf{type}$ gives the same two conclusions. Thus both conversion clauses are admissible. [/step] [step:Assemble the four admissible structural rules] The simultaneous induction proves the general substitution rule for every derivable judgment body $J$ over every context $\Gamma$. Weakening is the special case of this substitution rule for the projection $\rho:\Gamma,\Xi\to\Gamma$. Dependency-respecting exchange is the special case for the context isomorphism $\pi:\pi\Gamma\to\Gamma$ induced by the permitted permutation. The conversion clauses follow from the primitive conversion rule or from the assumed invariance under definitionally equal types. Therefore all four structural rules stated in the theorem are admissible for the standard dependent judgments of $\mathcal T$. [/step]