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

is mentioned by

Thm* L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List	[list-set-type2]
Thm* T:Type{i}, x:T, L:T List, P:(TTProp{i'}). Thm* (x,y[x / L].P(x,y))  (x,yL.P(x,y)) & (yL.P(x,y))	[pairwise-cons]
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