 Substitution is a crucial operation not only in first-order logics, but also in higher-order logics, as well as in other formal systems that contain a variable binding operator, such as the \(\lambda\)-calculi and the \(\varepsilon\)-calculus. Indeed, carrying out substitution correctly is particularly pressing in \(\lambda\)-calculi and in the closely related functional programming languages. CL can emulate \(\lambda\)-abstraction despite the fact that CL has no variable binding operators. This makes CL a suitable target language for functional programming languages to be compiled into.