IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter is nil2 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))
filter(P;v) ~ nil
By:
BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html