is mentioned by

Thm* f:(T1T2), Q:(T2), L:T1 List. Thm* filter(Q;map(f;L)) = map(f;filter(Q o f;L))

[filter_map]

In prior sections: fun 1 list 1 mb nat

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