IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
list decomp reverse11 1. T : Type
2. T List
0<||nil|| (x:T, L':T List. nil = (L' @ [x]))
By:
Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html