IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
absval elim
1
1
1. P : 
Prop
2. 
x:. P(|x|)
3. x : 
P(x)
| By: |
Inst: Hyp:-2 Using:[x] |
Generated subgoal:
| 1 |
4. P(|x|)
P(x)
 | 1 step |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
