is mentioned by

Thm* L:T List, x:T. x(x.L).False False	[list_all_of_false_false]
Def xL.P(x) == (letrec list_exists L = (Case of L; nil False ; h.t P(h) list_exists(t)) ) (L)	[list_exists]

In prior sections: core bool 1