IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi step at wf n:, f,g:({1...n}Peg), k:{1...n}. Moving disk k of n takes f to g Prop
By:
Def of Moving disk <nat> of <nat> takes <fun> to <fun>
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
n:
, f,g:({1...n}
Peg), k:{1...n}. Moving disk k of n takes f to g 
Prop
