Proposition/definition 49: For a statement \phi , we recursively define the iterated variable substitution \{\phi | a \to A, b \to B, ..., z \to Z\} as follows, where a, b, ..., z and A, B, ..., Z are lists of variables, each having as many items as the other.
(a) Base cases: \{\phi | a \to A, b \to B\} is the variable substitution \big[ [\phi | a \to A ] \big| b \to B \big]. (b) Recursion: Given variables a, b, ..., y, z and A, B, ..., Y, Z for which \{\phi | a \to A, b \to B, ..., y \to Y\} is known, we define \{\phi | a \to A, b \to B, ..., y \to Y, z \to Z\} to be \big[ \{\phi | a \to A, b \to B, ..., y \to Y\} \big| z \to Z \big]. It follows that \{ \phi | a \to A, b \to B, ..., z \to Z \} is defined for every statement \phi and for arbitrary variables a, b, ..., z and A, B, ..., Z .

Proof: We use structural induction over the definition of iterated variable substitution given above to show \{ \phi | a \to A, b \to B, ..., z \to Z \} is well-defined for arbitrary choices of variables a, b, ..., z and A, B, ..., Z .

Base cases: It was showed following the definition of variable substitution that [\phi | a \to A ] is a well-defined statement regardless of choices of \phi and variables a and A . It follows by the same result that \big[ [\phi | a \to A ] \big| b \to B \big] is then also well-defined. But this is the definition of \{ \phi | a \to A, b \to B \} .

Inductive step: We take as the induction hypothesis that \{\phi | a \to A, b \to B, …, y \to Y \} is well-defined, and need to show from this that \{\phi | a \to A, b \to B, …, y \to Y, z \to Z \} is then also well-defined. But the latter is the variable substitution \big[ \{ \phi | a \to A, b \to B, …, y \to Y \} \big| z \to Z \} \big], which, since \{\phi | a \to A, b \to B, …, y \to Y, z \to Z\} is well-defined by the induction hypothesis, we know itself is well-defined by the proof following the definition of variable substitution. \square