IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter is nil1 1. T : Type
2. P : T 3. T List
4. u : T 5. v : T List
6. (xv.P(x)) (filter(P;v) ~ nil)
7. P(u)
8. P(u) & (xv.P(x))
[u / filter(P;v)] ~ nil
By:
Analyze -1 THEN Analyze -2
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x
v.
P(x)) 
(filter(P;v) ~ nil)
[u / filter(P;v)] ~ nil
