Def (x:T. b(x))(x) == b(x)

is mentioned by

Thm* as:T List. (i:||as||. as[i]){||as||} = as	[listify_select_id]
Def For{T,op,id} x  as. f(x) == reduce(op;id;map(x:T. f(x);as))	[for]

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