Def (xL.P(x)) == x:T. (x  L) & P(x)

is mentioned by

Thm* f:(A), L:A List. 0<||L||  (aL.(xL.f(x)f(a)))

[maximal-in-list]

In prior sections: mb list 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html