1. y1 : 
2. y2 : 
3. <y1,y2> = <0,0>
4. <y1,y2> = <0,0>
  (next_nat_pair(prev_nat_pair(<y1,y2>)) = <0,0>  )  Prop

1

<y1,y2>  {xy:()| xy = <0,0>   }

1 step

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