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

is mentioned by

Thm* F:(AProp), L:A List. (k:A. Dec(F(k)))  Dec((kL.F(k)))	[decidable__l_all]
Thm* L1,L2:T List, P:(T). L2  filter(P;L1)  L2  L1 & (xL2.P(x))	[sublist_filter]
Thm* L:T List, P:(T). (xL.P(x))  reduce(x,y. P(x)y;true;L)	[l_all_reduce]
Thm* P:(TProp). (xnil.P(x))	[l_all_nil]
Thm* f:(AB), L:A List, P:(BProp). (xmap(f;L).P(x))  (xL.P(f(x)))	[l_all_map]
Thm* L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List	[list_set_type]
Thm* P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ nil)	[filter_is_nil]
Thm* P:(T), L:T List. (xL.P(x))  filter(P;L) = L	[filter_trivial2]
Thm* P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ L)	[filter_trivial]
Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y))	[l_all_cons]

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