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
7. u1 : T
8. v1 : T List
9. P:(T). v1  filter(P;[u / v])  v1  [u / v] & (xv1.P(x))
  P:(T). 
  [u1 / v1]  if P(u) [u / filter(P;v)] else filter(P;v) fi
  
  [u1 / v1]  [u / v] & (x[u1 / v1].P(x))

By:	Analyze 0 THEN RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y)) 0 THEN SplitOnConclITE

1	10. P : T 11. P(u)   [u1 / v1]  [u / filter(P;v)]  [u1 / v1]  [u / v] & P(u1) & (xv1.P(x))	10 steps
2	10. P : T 11. P(u)   [u1 / v1]  filter(P;v)  [u1 / v1]  [u / v] & P(u1) & (xv1.P(x))	9 steps

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