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