Definition 28: We define the simple multiple variable substitution $$[\phi | a \to A, b \to B, ..., z \to Z]_\textup{simple}$$recursively as follows, where $\phi$ is a statement and $a, b, ..., z$ and $A, B, ..., Z$ are lists of variables, each having the same length.
(a) Base cases: $[\phi | a \to A, b \to B]_\textup{simple}$ is the variable substitution $$\big[ [\phi | a \to A ] \big| b \to B \big].$$(b) Recursion: Given variables $a, b, ..., y, z, A, B, ..., y, Z$ such that $$[\phi | a \to A, b \to B, ..., y \to Y]_\textup{simple}$$is known, we define $$[\phi | a \to A, b \to B, ..., y \to Y, z \to Z]$$to be given by $$\big[ [\phi | a \to A, b \to B, ..., y \to Y]_\textup{simple} \big| z \to Z \big].$$