IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter iseg T:Type, P:(T), L2,L1:T List. L1L2 filter(P;L1) filter(P;L2)
By:
RepeatFor 3 (Analyze 0) THEN ListInd -1 THEN Reduce 0
1. T : Type
2. P : T 3. T List
4. u : T 5. v : T List
6. L1:T List. L1v 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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html