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)

By:	Def of <int>=<int> | otherPeg(<Peg>; <Peg>)

1

1. p : {1...3} 2. r : {1...3} 3. q : {1...3} 4. s : {1...3} 5. p  q 6. r  s   Inj({1...3}; {1...3};   Inj(u.if if u=p true ; false fi r   Inj(u.i; if u=q true ; false fi s   Inj(u.else 6-(r+s) fi)

2 steps

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