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