IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc find intlist great bound112121a11 1. List
2. u :
3. v : List
4. w :
5. i:||v||. v[i]<w 6. u<w 7. i : ||u.v||
8. 0<i v[(i-1)]<u+2
By:
Inst: Hyp:5 Using:[i-1]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html