Proposition 35: Given variables x and y together with statements \alpha, \beta, ..., \omega , the variable substitution \big[ (\alpha \vee \beta \vee \cdots \vee \omega) \big| x \to y \big], where we have used iterated disjunction, is given by \big( [\alpha | x \to y] \vee [\beta | x \to y] \vee \cdots \vee [\omega | x \to y] \big).

Proof: We shall argue by structural induction over the definition of iterated disjunctions.

Base cases: For statements \alpha , \beta and \gamma , recall that (\alpha \vee \beta \vee \gamma) is defined as the disjunction \big( (\alpha \vee \beta) \vee \gamma \big) . By [34], \big[ (\alpha \vee \beta \vee \gamma) \big| x \to y\big] is given by \Big( \big[ (\alpha \vee \beta) \big| x \to y \big] \vee [\gamma | x \to y] \Big). But \big[ (\alpha \vee \beta) \big| x \to y \big] is given by \big( [\alpha | x \to y] \vee [\beta | x \to y] \big) , so the above is \Big( \big( [\alpha | x \to y] \vee [\beta | x \to y] \big) \vee [\gamma | x \to y] \Big). This is precisely the definition of \big( [\alpha | x \to y] \vee [\beta | x \to y] \vee [\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 then also known for the statements \alpha, \beta, ..., \psi, \omega . As (\alpha \vee \beta \vee \cdots \vee \psi \vee \gamma) is given by \big( (\alpha \vee \beta \vee \cdots \vee \psi) \vee \omega \big), it follows by [34] that \big[ (\alpha \vee \beta \vee \cdots \vee \psi \vee \omega ) \big| x \to y \big] is given by \Big( \big[ (\alpha \vee \beta \vee \cdots \vee \psi) \big| x \to y \big] \vee [\omega | x \to y] \Big). Using the induction hypothesis, this is the same as \Big( \big( [\alpha | x \to y] \vee [\beta | x \to y] \vee \cdots \vee [\psi|x \to y] \big) \vee [\omega | x \to y] \Big), i.e. \big( [\alpha | x \to y] \vee [\beta | x \to y] \vee \cdots \vee [\psi|x \to y] \vee [\omega | x \to y] \big) . \square