IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
increasing implies12 1. k : 2. f : k 3. i:(k-1). f(i)<f(i+1)
4. x : k 5. y : k 6. x<y 7. d:, a,b:k. b-a = d+1 f(a)<f(b)
f(x)<f(y)
By:
Using [`d',(y-x-1)] BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html