IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
next nat pair vs prev nat pair11 1. x1 : 2. x2 : 3. x2 = 0
<x1+1-1,0> = <x1,x2>
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
<x1+1-1,0> = <x1,x2> 
