Proposition 37: Given variables x and y together with statements \alpha, \beta, ..., \omega , the variable substitution \big[ (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \omega) \big| x \to y \big], where we have used an implication chain, is given by \big( [\alpha | x \to y] \Rightarrow [\beta | x \to y] \Rightarrow \cdots \Rightarrow [\omega | x \to y] \big).

Proof: We use structural induction over the definition of implication chains.

Base cases: For statements \alpha , \beta and \gamma , recall that (\alpha \Rightarrow \beta \Rightarrow \gamma) is defined as the conjunction pf implications \big( (\alpha \Rightarrow \beta) \wedge (\beta \Rightarrow \gamma ) \big). By definition of variable substitution, \big[ (\alpha \Rightarrow \beta \Rightarrow \gamma) \big| x \to y\big] is given by \Big( \big[ (\alpha \Rightarrow \beta) \big| x \to y \big] \wedge \big[(\beta \Rightarrow \gamma) \big| x \to y\big] \Big). But \big[ (\alpha \Rightarrow \beta) \big| x \to y \big] and \big[ (\beta \Rightarrow \gamma) \big| x \to y \big] are by [36] given by \big( [\alpha | x \to y] \Rightarrow [\beta | x \to y] \big) \hspace{3mm} \textup{and} \hspace{3mm} \big( [\beta | x \to y] \Rightarrow [\gamma | x \to y] \big), respectively, meaning that the above is \Big( \big( [\alpha | x \to y] \Rightarrow [\beta | x \to y] \big) \wedge \big( [\beta | x \to y] \Rightarrow [\gamma | x \to y] \big) \Big). This is precisely the definition of \big( [\alpha | x \to y] \Rightarrow [\beta | x \to y] \Rightarrow [\gamma|x \to y]\big) .

Inductive step: We take as the induction hypothesis that the desired result is known for the statements \alpha, \beta, ..., \psi , and need to show from this that it is also known for the statements \alpha, \beta, ..., \psi, \omega . As (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi \Rightarrow \gamma) is given by \big( (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi) \wedge (\psi \Rightarrow \omega) \big), it follows by definition of variable substitution that \big[ (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi \Rightarrow \omega ) \big| x \to y \big] is given by \Big( \big[ (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi) \big| x \to y \big] \wedge \big[ ( (\psi \Rightarrow \omega) \big| x \to y \big] \Big). Using the induction hypothesis and [36], this is the same as \begin{align*} \Big( \big( [\alpha | x \to y] \Rightarrow [\beta | x \to y] \Rightarrow \cdots& \Rightarrow [\psi|x \to y] \big) \\[1.5mm] \wedge& \big( [\psi | x \to y] \Rightarrow [\omega | x \to y] \big) \Big), \end{align*} i.e. \big( [\alpha | x \to y] \Rightarrow [\beta | x \to y] \Rightarrow \cdots \Rightarrow [\psi|x \to y] \Rightarrow [\omega | x \to y] \big) . \square