(4steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi otherpeg diff2
  x,y:Peg. x  y  otherPeg(x; y)  y
By: Auto

Generated subgoal:

1 1. x : Peg
2. y : Peg
3. x  y
  otherPeg(x; y)  y
3 steps

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

(4steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc