is mentioned by

Def xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L)

[list_all]

In prior sections: core discrete jlc core 3 jlc bool 1