[proofplan]
We prove the result by simultaneous induction on derivations, because substitution must preserve both judgments and the well-formedness of the dependent context following the substituted variable. The central case is the variable rule: the distinguished variable $x$ is replaced by the given derivation of $a:A$, while variables declared before or after $x$ are transported to the substituted context with their types substituted. All formation, introduction, elimination, and equality rules are then handled uniformly by applying the induction hypotheses to their premises and reapplying the same rule to the substituted premises, with alpha-renaming used before substitution whenever a binder would otherwise capture a free variable of $a$.
[/proofplan]
[step:Set up simultaneous induction on derivations and context formation]
Fix a derivation
\begin{align*}
\mathcal D:\Gamma,x:A,\Delta \vdash J
\end{align*}
and a derivation
\begin{align*}
\mathcal A:\Gamma \vdash a:A.
\end{align*}
Here $\mathcal D$ denotes a formal derivation tree, and $\mathcal A$ denotes the given derivation of the substituting term.
We prove, simultaneously for every finite dependent context tail $\Theta$ and every judgment $K$ over $\Gamma,x:A,\Theta$, the following assertion:
\begin{align*}
\text{if } \Gamma,x:A,\Theta \vdash K \text{ is derivable, then } \Gamma,\Theta[a/x]\vdash K[a/x] \text{ is derivable.}
\end{align*}
The simultaneous induction also includes the context-formation assertion:
\begin{align*}
\text{if } \Gamma,x:A,\Theta \text{ is well formed, then } \Gamma,\Theta[a/x] \text{ is well formed.}
\end{align*}
This simultaneous form is necessary because the type of a later variable in $\Theta$ may contain $x$, so a later variable rule can only be reconstructed after the corresponding substituted context entry has already been proved well formed. The induction is on the final rule of the derivation tree, with the context-formation cases interleaved with the judgment cases.
[/step]
[step:Substitute through context extension]
Consider a context-formation derivation ending by adjoining a fresh variable $y:B$ to a well-formed context $\Gamma,x:A,\Theta$. Thus the premises are that $\Gamma,x:A,\Theta$ is well formed, that
\begin{align*}
\Gamma,x:A,\Theta \vdash B\ \mathsf{type}
\end{align*}
is derivable, and that $y$ is fresh for $\Gamma,x:A,\Theta$.
By the induction hypothesis for context formation, $\Gamma,\Theta[a/x]$ is well formed. By the induction hypothesis for the type judgment,
\begin{align*}
\Gamma,\Theta[a/x]\vdash B[a/x]\ \mathsf{type}
\end{align*}
is derivable. Since substitution is capture avoiding, and bound or declared variables are alpha-renamed before substitution when necessary, the variable $y$ may be chosen fresh for $\Gamma,\Theta[a/x]$. Therefore the context-extension rule gives that
\begin{align*}
\Gamma,\Theta[a/x],y:B[a/x]
\end{align*}
is well formed. This is exactly the substituted context
\begin{align*}
(\Gamma,x:A,\Theta,y:B)[a/x]=\Gamma,\Theta[a/x],y:B[a/x].
\end{align*}
[/step]
[step:Handle the variable rule by separating variables before at and after the substitution point]
Suppose the final rule of the derivation is a variable rule. There are three cases.
First, let the variable be the distinguished variable $x$. The original conclusion is
\begin{align*}
\Gamma,x:A,\Theta \vdash x:A.
\end{align*}
After substitution, this judgment becomes
\begin{align*}
\Gamma,\Theta[a/x]\vdash a:A.
\end{align*}
The derivation $\mathcal A:\Gamma\vdash a:A$ is given. Since the simultaneous context-formation induction has established that $\Gamma,\Theta[a/x]$ is a well-formed extension of $\Gamma$, the admissible use of a derivation over an earlier context inside a well-formed later context gives
\begin{align*}
\Gamma,\Theta[a/x]\vdash a:A.
\end{align*}
Second, let the variable $y$ be declared in $\Gamma$. Its type $B$ is declared before $x$, so $B[a/x]=B$. The original variable rule gives
\begin{align*}
\Gamma,x:A,\Theta \vdash y:B.
\end{align*}
Since $y:B$ is still an entry of the prefix $\Gamma$ in the substituted context $\Gamma,\Theta[a/x]$, the variable rule gives
\begin{align*}
\Gamma,\Theta[a/x]\vdash y:B.
\end{align*}
Third, let the variable $y$ be declared in the tail $\Theta$. Write the relevant decomposition of the tail as
\begin{align*}
\Theta=\Theta_0,y:B,\Theta_1,
\end{align*}
where $B$ is a type over $\Gamma,x:A,\Theta_0$. The variable rule in the original context gives
\begin{align*}
\Gamma,x:A,\Theta_0,y:B,\Theta_1 \vdash y:B.
\end{align*}
By the context-substitution part of the simultaneous induction, the substituted context
\begin{align*}
\Gamma,\Theta_0[a/x],y:B[a/x],\Theta_1[a/x]
\end{align*}
is well formed. Applying the variable rule in this context gives
\begin{align*}
\Gamma,\Theta_0[a/x],y:B[a/x],\Theta_1[a/x]\vdash y:B[a/x].
\end{align*}
This is precisely the substituted judgment.
[guided]
The variable rule is the only case where substitution changes the source of a variable judgment, so we treat it in detail.
Fix a variable-rule conclusion in a context of the form $\Gamma,x:A,\Theta$. There are three possible locations for the variable. If the variable is $x$ itself, then the original judgment is
\begin{align*}
\Gamma,x:A,\Theta \vdash x:A.
\end{align*}
Substituting $a$ for $x$ changes the term $x$ into $a$ and removes the declaration $x:A$ from the context, so the desired conclusion is
\begin{align*}
\Gamma,\Theta[a/x]\vdash a:A.
\end{align*}
We already have $\mathcal A:\Gamma\vdash a:A$. The simultaneous induction on contexts gives that $\Gamma,\Theta[a/x]$ is a well-formed extension of $\Gamma$. Hence the derivation of $a:A$ over $\Gamma$ remains valid in this later well-formed context, so
\begin{align*}
\Gamma,\Theta[a/x]\vdash a:A
\end{align*}
is derivable.
If the variable is a variable $y$ declared before $x$, then $y:B$ is an entry of $\Gamma$. The type $B$ does not depend on $x$, because $x$ has not yet been declared when $B$ is formed. Therefore $B[a/x]=B$. Since the prefix $\Gamma$ is unchanged in the substituted context, the variable rule directly gives
\begin{align*}
\Gamma,\Theta[a/x]\vdash y:B.
\end{align*}
If the variable is declared after $x$, write the context tail as
\begin{align*}
\Theta=\Theta_0,y:B,\Theta_1.
\end{align*}
Here $B$ may depend on $x$ and on the earlier part $\Theta_0$, so substituting affects the declared type of $y$. The substituted context has the form
\begin{align*}
\Gamma,\Theta_0[a/x],y:B[a/x],\Theta_1[a/x].
\end{align*}
The context-formation part of the simultaneous induction proves that this context is well formed. Now the variable rule applies to the displayed declaration $y:B[a/x]$ and yields
\begin{align*}
\Gamma,\Theta_0[a/x],y:B[a/x],\Theta_1[a/x]\vdash y:B[a/x].
\end{align*}
This is exactly the result of substituting $a$ for $x$ in the original variable judgment.
[/guided]
[/step]
[step:Reconstruct every nonbinding rule from substituted premises]
Consider an inference rule whose premises and conclusion contain no new binder. Its derivation has premises of the form
\begin{align*}
\Gamma,x:A,\Theta_i \vdash K_i
\end{align*}
for finitely many indices $i$, and conclusion
\begin{align*}
\Gamma,x:A,\Theta \vdash K.
\end{align*}
The rule is one of the type-formation, introduction, elimination, computation, or equality rules of the theory, and its syntactic substitution instance is again an instance of the same rule.
By the induction hypothesis applied to each premise, every substituted premise
\begin{align*}
\Gamma,\Theta_i[a/x]\vdash K_i[a/x]
\end{align*}
is derivable. The rule is stable under capture-avoiding substitution, so applying the same inference rule to these substituted premises gives
\begin{align*}
\Gamma,\Theta[a/x]\vdash K[a/x].
\end{align*}
This proves the induction step for all nonbinding rule instances.
[/step]
[step:Rename bound variables before substituting through binding rules]
Now consider a rule whose conclusion introduces or eliminates a binder, such as a dependent function type, a lambda abstraction, a dependent pair eliminator, or an identity eliminator. Let $y$ denote a bound variable introduced in such a rule. Before applying the induction hypothesis, alpha-rename $y$ if necessary so that $y$ is distinct from $x$, is not declared in $\Gamma$ or $\Delta$, and does not occur free in the substituting term $a$.
Alpha-renaming does not change the represented judgment, and capture-avoiding substitution is defined after such renaming. Therefore substitution commutes with the syntactic formation of the rule instance: the premises of the substituted rule are exactly the substitutions of the original premises, and the conclusion of the substituted rule is exactly the substitution of the original conclusion.
Applying the induction hypothesis to each renamed premise gives the corresponding substituted premise. Reapplying the same binding rule then gives the substituted conclusion. Thus all binding type-formers, term constructors, eliminators, and computation rules are preserved by substitution.
[/step]
[step:Substitute through definitional equality and conversion judgments]
For a definitional equality of types or terms, the final rule is either a primitive equality rule, a congruence rule, a computation rule, a symmetry rule, a transitivity rule, or a conversion rule. In every case, the premises are derivable judgments over contexts of the form $\Gamma,x:A,\Theta_i$.
By the induction hypothesis, each premise remains derivable after replacing its context by $\Gamma,\Theta_i[a/x]$ and its judgment by the corresponding substituted judgment. The equality rules are schematic in their displayed terms and types, so the same equality, congruence, computation, symmetry, transitivity, or conversion rule applies to the substituted premises. Hence the substituted equality or converted typing judgment is derivable in the substituted context.
[/step]
[step:Conclude the substituted judgment]
The preceding cases cover the possible final rules in the derivation tree of
\begin{align*}
\Gamma,x:A,\Delta \vdash J.
\end{align*}
By induction on that derivation, and simultaneously on the formation of the dependent context tail, we obtain both that $\Gamma,\Delta[a/x]$ is well formed and that
\begin{align*}
\Gamma,\Delta[a/x]\vdash J[a/x]
\end{align*}
is derivable. This is the required substitution rule.
[/step]
