IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter is nil T:Type, P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ nil)
By:
RepeatFor 3 (Analyze 0) THEN ListInd -1 THEN Reduce 0 THEN Try (Complete Auto)
THEN
Reduce 0
THEN
SplitOnConclITE
THEN
Analyze 0
THEN
RWO Thm*P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y)) -1