It is because of the way set comprehension works.
{b':Books | b' = Books - b }
This expression delivers all the singleton subsets of Books
which are equal to Books - b
. But Books - b
is a two-element set. So no singleton set is equal to it and the overall result is {}
.
You probably simply want:
fun f[b:Books] : Books {
Books - b
}