IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
int upper well founded11 1. n :
2. WellFnd{i}({n...};x,y.x-n<y-n)
WellFnd{i}({n...};x,y.x<y)
By:
Rewrite-1 by x,y:{n...}. x-n<y-nx<y
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html