IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter trivial2 1. T : Type
2. P : T 3. T List
4. u : T 5. v : T List
6. (xv.P(x)) (filter(P;v) ~ v)
7. P(u)
8. P(u) & (xv.P(x))
filter(P;v) ~ [u / v]
By:
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) ~ v)
P(u)
filter(P;v) ~ [u / v]
