IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi seq wf n:, a,z:, s:({a...z}{1...n}Peg).
s is a Hanoi(n disk) seq on a..z Prop
By:
Def of <function> is a Hanoi(<num> disk) seq on <int>..<int>
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
n:
, a,z:
, s:({a...z}
{1...n}
s is a Hanoi(n disk) seq on a..z 
Prop
