T:Type, P:(T), T':Type, f:({x:T| P(x) }T'), L:T List.
  mapfilter(f;P;L)  T' List

By:	Auto THEN Unfold `mapfilter` 0 THEN Inst Thm* T:Type, P:(T), l:T List. filter(P;l)  {x:T| P(x) } List [T;P;L]

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html