1. k,x,y:. x+y = k  (a:. nat_to_nat_pair(a) = <x,y>)
  b:(). a:. nat_to_nat_pair(a) = b

1

2. x :  3. y :    a:. nat_to_nat_pair(a) = <x,y>

1 step

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