T:Type, P:(T), L2,L1:T List. L1  L2  filter(P;L1)  filter(P;L2)

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

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