(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 1
1. x : Peg
2. y : Peg
3. x  y
  otherPeg(x; y)  y
By: Rewrite by Thm*  x,y:Peg. x  y  otherPeg(x; y) = otherPeg(y; x)

Generated subgoal:

1   otherPeg(y; x)  y
2 steps

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

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