1. T : Type
2. T List
3. T List
4. u : T
5. v : T List
6. P:(T). v  filter(P;nil)  v  nil & (xv.P(x))
  P:(T). [u / v]  nil  [u / v]  nil & (x[u / v].P(x))

By:	RWO Thm* x:T, L:T List. [x / L]  nil  False 0

None

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