Nuprl - Proof: hanoi peg perm is inj

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi peg perm is inj

p,r,q,s:Peg. p

Inj(Peg; Peg; permute(p to r ; q to s))

By:	Def of Peg \| permute(p to r ; q to s)

Generated subgoal:

1   p,r,q,s:{1...3}.
  p  q

  r  s

  Inj({1...3}; {1...3}; u.if u=p r ; u=q s else otherPeg(r; s) fi)
3 steps

About:

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