IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
next nat pair vs prev nat pair2121121 1. y1 : 2. y2 : 3. <y1,y2> = <0,0>
4. <y1-1+1,y2+1-1> = <0,0>
5. y1 0
6. y2+1 0
<y1,y2> = <0,0>
By:
Analyze-3 THEN Reduce Hyp:-3 THEN Reduce Hyp:4
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html