is mentioned by

Def (xL.P(x)) == reduce(x,b. P(x) b;false;L)

[l_bexists]

In prior sections: bool 1 num thy 1

Try larger context: Graphs