 Now we give a concrete example to illustrate how to turn a formula of FOL into one that contains only \(\mid^-\), and then how to eliminate the bound variables using \(U\) and combinators. To put some excitement into the process, we start with the sentence in (#1).