IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi seq deepen higheq1 1. a : 2. z : 3. n : 4. s : {a...z}{1...n}Peg
5. n' : 6. nn' 7. h : {n+1...n'}Peg
8. i : {1...n'}
9. n<i 10. x : {a...z}
(s(x) {to n} h {to n'})(i) = h(i)