T:Type, P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x)

1	1. T : Type 2. P : T 3. T List   x:T. (x  nil)  (x  nil) & P(x)	1 step
2	1. T : Type 2. P : T 3. T List 4. u : T 5. v : T List 6. x:T. (x  filter(P;v))  (x  v) & P(x)   x:T.    (x  if P(u) [u / filter(P;v)] else filter(P;v) fi)  (x  [u / v]) & P(x)	13 steps

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