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_exists]
Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x)  (yL.P(y))	[l_exists_cons]
Thm* P:(TProp). (xnil.P(x))  False	[l_exists_nil]

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