IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter trivial1 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))
[u / filter(P;v)] ~ [u / v]
By:
Analyze THEN Try Trivial THEN BackThruSomeHyp
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)
[u / filter(P;v)] ~ [u / v]
