1. T : Type
2. T List
3. u : T
4. v : T List
5. L2:T List, P:(T). L2  filter(P;v)  L2  v & (xL2.P(x))
6. T List
  P:(T). 
  nil  if P(u) [u / filter(P;v)] else filter(P;v) fi
  
  nil  [u / v] & (xnil.P(x))

By:	RWO Thm* L:T List. nil  L  True 0 THEN Easy

None

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