1. n : 
2. f : {1...n}Peg
3. g : {1...n}Peg
4. f(n) = g(n)
5. a : 
6. z : {a...}
7. s : {a...z}{1...n-1}Peg
8. s is a Hanoi(n-1 disk) seq on a..z
9. s(a) = f
10. s(z) = g
  s:({a...z}{1...n}Peg). 
  s is a Hanoi(n disk) seq on a..z
  & s(a) = f  {1...n}Peg
  & s(z) = g  {1...n}Peg

By:	Witness: s(?) {to n-1}  i.f(n) {to n}

1	(s(?) {to n-1}  i.f(n) {to n}) is a Hanoi(n disk) seq on a..z	1 step
2	(s(?) {to n-1}  i.f(n) {to n})(a) = f	6 steps
3	(s(?) {to n-1}  i.f(n) {to n})(z) = g	6 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html