Def map(f;as) == Case of as; nil  nil ; a.as'  f(a).map(f;as')  (recursive)

is mentioned by

Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n])	[map_select]
Thm* as:A List. map(Id;as) = as	[map_id]
Thm* f:(AB), as,as':A List. map(f;as @ as') = (map(f;as) @ map(f;as'))	[map_append]
Thm* f:(AB), g:(BC), as:A List. map(g;map(f;as)) = map(g o f;as)	[map_map]
Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||	[map_length]
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