Definition 27: 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].