[proofplan] We prove the statement by induction on the derivation of $\Gamma,x:A \vdash t:B$. The variable case uses the distinctness of context declarations to separate the substituted variable $x$ from every other variable in $\Gamma$. The application case follows by applying the induction hypotheses to the two immediate subderivations and rebuilding the typing derivation with the application rule. The abstraction case is the only point where capture avoidance matters: we alpha-rename the bound variable to be fresh, weaken the typing derivation of $s$, apply the induction hypothesis under the extended context, and then rebuild the abstraction. [/proofplan] [step:Prove the lemma by induction on the typing derivation] Fix a typing context $\Gamma$, a variable $x \notin \operatorname{dom}(\Gamma)$, terms $t,s \in \textsf{Tm}$, and simple types $A,B \in \textsf{Ty}$. Assume \begin{align*} \Gamma,x:A \vdash t:B \end{align*} and \begin{align*} \Gamma \vdash s:A. \end{align*} We prove \begin{align*} \Gamma \vdash t[s/x]:B \end{align*} by induction on the given derivation $\mathcal{D}$ of $\Gamma,x:A \vdash t:B$. The induction statement is slightly more general at the recursive calls: whenever a derivation has conclusion \begin{align*} \Delta,x:A \vdash r:C \end{align*} and $\Delta \vdash s:A$, with $x \notin \operatorname{dom}(\Delta)$, the conclusion is \begin{align*} \Delta \vdash r[s/x]:C. \end{align*} This formulation is needed because the abstraction case applies the induction hypothesis under an extended context. [/step] [step:Handle the variable rule by separating the substituted variable from the other variables] Suppose the last rule of $\mathcal{D}$ is the variable rule. Then $t$ is a variable; write it as $z$. Since \begin{align*} \Gamma,x:A \vdash z:B \end{align*} is derived by the variable rule, the declaration $z:B$ occurs in the context $\Gamma,x:A$. If $z=x$, then the pairwise distinctness of the context gives $B=A$. By the definition of capture-avoiding substitution on variables, \begin{align*} x[s/x]=s. \end{align*} The assumed derivation $\Gamma \vdash s:A$ is therefore exactly \begin{align*} \Gamma \vdash x[s/x]:B. \end{align*} If $z \neq x$, then the declaration $z:B$ must occur in $\Gamma$, because the only declaration added after $\Gamma$ is $x:A$ and context variables are pairwise distinct. Hence the variable rule gives \begin{align*} \Gamma \vdash z:B. \end{align*} Since $z \neq x$, capture-avoiding substitution on variables gives \begin{align*} z[s/x]=z. \end{align*} Thus \begin{align*} \Gamma \vdash z[s/x]:B. \end{align*} [guided] Suppose the final rule in the derivation is the variable rule. Then the term being typed is a variable, so write $t=z$ for a variable $z$. The conclusion \begin{align*} \Gamma,x:A \vdash z:B \end{align*} means precisely that the declaration $z:B$ appears in the finite context $\Gamma,x:A$. There are two cases. First assume $z=x$. Since contexts contain pairwise distinct variables and $x$ was added with type $A$, the declaration for $x$ in $\Gamma,x:A$ is uniquely $x:A$. Therefore $B=A$. The definition of capture-avoiding substitution on the variable being substituted says \begin{align*} x[s/x]=s. \end{align*} The hypothesis already gives \begin{align*} \Gamma \vdash s:A. \end{align*} Since $B=A$, this is exactly the required judgment \begin{align*} \Gamma \vdash x[s/x]:B. \end{align*} Now assume $z \neq x$. The declaration $z:B$ cannot be the final declaration $x:A$, because the variables are different. Hence $z:B$ occurs in $\Gamma$. Applying the variable rule in the smaller context gives \begin{align*} \Gamma \vdash z:B. \end{align*} The definition of substitution on a different variable says \begin{align*} z[s/x]=z. \end{align*} Therefore \begin{align*} \Gamma \vdash z[s/x]:B. \end{align*} This proves the variable case. [/guided] [/step] [step:Push substitution through an application and rebuild the application typing] Suppose the last rule of $\mathcal{D}$ is the application rule. Then there are a term $r \in \textsf{Tm}$, a term $u \in \textsf{Tm}$, and a type $C \in \textsf{Ty}$ such that \begin{align*} t=r\,u \end{align*} and the immediate subderivations are \begin{align*} \Gamma,x:A \vdash r:C \to B \end{align*} and \begin{align*} \Gamma,x:A \vdash u:C. \end{align*} By the induction hypothesis applied to the first subderivation and to $\Gamma \vdash s:A$, \begin{align*} \Gamma \vdash r[s/x]:C \to B. \end{align*} By the induction hypothesis applied to the second subderivation and to $\Gamma \vdash s:A$, \begin{align*} \Gamma \vdash u[s/x]:C. \end{align*} The application typing rule gives \begin{align*} \Gamma \vdash r[s/x]\,u[s/x]:B. \end{align*} By the recursive definition of capture-avoiding substitution on applications, \begin{align*} (r\,u)[s/x]=r[s/x]\,u[s/x]. \end{align*} Since $t=r\,u$, we conclude \begin{align*} \Gamma \vdash t[s/x]:B. \end{align*} [/step] [step:Rename the bound variable in the abstraction case to avoid capture] Suppose the last rule of $\mathcal{D}$ is the abstraction rule. Then there are a variable $y$, a term $r \in \textsf{Tm}$, and simple types $C,D \in \textsf{Ty}$ such that \begin{align*} t=\lambda y:C.\,r \end{align*} and \begin{align*} B=C \to D. \end{align*} The immediate subderivation is \begin{align*} \Gamma,x:A,y:C \vdash r:D. \end{align*} Because terms are identified up to alpha-equivalence and substitution is capture-avoiding, choose the representative of the abstraction so that $y$ is fresh for $x$, fresh for $\Gamma$, and not free in $s$. With this choice, $x \notin \operatorname{dom}(\Gamma,y:C)$ and capture-avoiding substitution satisfies \begin{align*} (\lambda y:C.\,r)[s/x]=\lambda y:C.\,r[s/x]. \end{align*} From $\Gamma \vdash s:A$, the [Weakening Rule]([citetheorem:9622]) applied to the fresh declaration $y:C$ gives \begin{align*} \Gamma,y:C \vdash s:A. \end{align*} Apply the induction hypothesis to the subderivation \begin{align*} \Gamma,y:C,x:A \vdash r:D \end{align*} after using the admissible exchange of independent fresh declarations to regard the displayed subderivation equivalently with the context ordered as $\Gamma,y:C,x:A$. Equivalently, because $y$ is fresh and the simple type $C$ does not depend on $x$, the same derivation of the body is available under the context $\Gamma,y:C,x:A$. The induction hypothesis yields \begin{align*} \Gamma,y:C \vdash r[s/x]:D. \end{align*} By the abstraction typing rule, \begin{align*} \Gamma \vdash \lambda y:C.\,r[s/x]:C \to D. \end{align*} Since $B=C \to D$ and $(\lambda y:C.\,r)[s/x]=\lambda y:C.\,r[s/x]$, this is \begin{align*} \Gamma \vdash t[s/x]:B. \end{align*} [guided] Suppose the final rule is the abstraction rule. Then the term has the form \begin{align*} t=\lambda y:C.\,r \end{align*} for a variable $y$, a body term $r \in \textsf{Tm}$, and simple types $C,D \in \textsf{Ty}$, with \begin{align*} B=C \to D. \end{align*} The typing rule for abstraction says that the derivation ends with a derivation of the body: \begin{align*} \Gamma,x:A,y:C \vdash r:D. \end{align*} The possible difficulty is capture. If the bound variable $y$ occurred free in $s$, then substituting $s$ into the body under $\lambda y:C$ could accidentally bind a free occurrence of $y$ in $s$. The statement avoids this problem by using capture-avoiding substitution and identifying terms up to alpha-equivalence. Therefore we may replace the abstraction by an alpha-equivalent one and assume that $y$ is fresh for $x$, fresh for the variables already in $\Gamma$, and not free in $s$. With this representative, substitution passes under the binder: \begin{align*} (\lambda y:C.\,r)[s/x]=\lambda y:C.\,r[s/x]. \end{align*} To apply the induction hypothesis to the body, we need the substituting term $s$ to be well typed in the context where the new bound variable has been added. We know \begin{align*} \Gamma \vdash s:A. \end{align*} Since $y$ is fresh for $\Gamma$, the [Weakening Rule]([citetheorem:9622]) permits adding the unused declaration $y:C$ to the context, giving \begin{align*} \Gamma,y:C \vdash s:A. \end{align*} The body derivation has the assumptions $x:A$ and $y:C$ both present. Because $y$ is fresh and the type $C$ is simple, the declaration $y:C$ does not depend on $x$. Thus the independent declarations $x:A$ and $y:C$ may be regarded in the order needed for the induction hypothesis, namely as a derivation \begin{align*} \Gamma,y:C,x:A \vdash r:D. \end{align*} Now the induction hypothesis applies with $\Delta=\Gamma,y:C$, term $r$, substituted variable $x$, substituting term $s$, source type $A$, and target type $D$. It gives \begin{align*} \Gamma,y:C \vdash r[s/x]:D. \end{align*} Finally we rebuild the abstraction. The abstraction typing rule applied to the last judgment yields \begin{align*} \Gamma \vdash \lambda y:C.\,r[s/x]:C \to D. \end{align*} Since $B=C \to D$ and capture-avoiding substitution under the fresh binder gives \begin{align*} (\lambda y:C.\,r)[s/x]=\lambda y:C.\,r[s/x], \end{align*} we obtain \begin{align*} \Gamma \vdash t[s/x]:B. \end{align*} This proves the abstraction case. [/guided] [/step] [step:Conclude the induction over all typing rules] The typing rules for the simply typed lambda calculus with function types are exactly the variable, application, and abstraction rules. The preceding steps prove the desired substitution conclusion in each possible final-rule case of the derivation $\mathcal{D}$. By induction on $\mathcal{D}$, whenever \begin{align*} \Gamma,x:A \vdash t:B \end{align*} and \begin{align*} \Gamma \vdash s:A, \end{align*} we have \begin{align*} \Gamma \vdash t[s/x]:B. \end{align*} This is the claimed substitution lemma. [/step]