IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
reverse wf2 1. T : Type
2. T List
3. u : T 4. v : T List
5. rev(v) T List
(rev(v) @ [u]) T List
By:
Analyze
Generated subgoals:
1
rev(v) T List
Trivial
2
[u] T List
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T List
(rev(v) @ [u]) 
