A note on mechanizing higher order logic

It seems most unlikely that one could in general write purely applicative Schonfmkel descriptions', like (5), of functions already known to one in some other form. Fortunately there is a general procedure -- the Schonfmkel procedure -- which, when applied to any expression written in the more intuitive lambda-calculus notation, will produce a correct translation of it into the Schonfinkel notation.