is mentioned by

Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'. Thm* (x  mapfilter(f;P;L))  (y:T. (y  L) & P(y) & x = f(y))

[member_map_filter]

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