En el ejemplo del capitulo 2.8 de The Haskell Road To Logic, Math and Programming, la formula:

∀x ∈ {1,2,3} ∃y ∈ {1,4,9} x = y²

Se codifica como:

every, some :: [a] -> (a -> Bool) -> Bool
every xs p = all p xs
some xs p = any p xs
every [1,4,9] (\x -> some [1,2,3] (\y -> x = y^2))

Después en el Ej 2.51 se propone definir una función unique :: (a -> Bool) -> [a] -> Bool
que retorne True para unique p xs solo cuando haya un solo elemento de xs que cumpla con p.

La forma obvia de resolverlo es:

unique :: (a -> Bool) -> [a] -> Bool
unique p [] = False
unique p xs = length(filter p xs) == 1

Que se puede testear con:

unique (\x -> x>4) [1,2,3,4,5]
True
unique (\x -> x>4) [1,2,3,4,5,6]
False

Sin embargo es interesante pensarlo en la formula de Russell para Unicidad: ∃x ( Φ(x) ∧ ∀y ( Φ(y) => x=y ) ) . Que se puede hacer como:

unique1 :: (Eq a) => (a -> Bool) -> [a] -> Bool
unique1 p xs = some xs (\x -> p x && every xs (\y -> p y ==> x == y))
unique1 (\x -> x>4) [1,2,3,4,5]
True
unique1 (\x -> x>4) [1,2,3,4,5,6]
False

Lo interesante es que usando expresiones lambda llegamos a una formula que expresa prácticamente idéntica la original.