IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose increasing11 1. k : 2. m : 3. f : km 4. g : m 5. increasing(f;k)
6. increasing(g;m)
7. i : (k-1)
8. x,y:m. x<yg(x)<g(y)
f(i)<f(i+1)
By:
AllHyps (i.Unfold `increasing` i THEN BackThru i)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x,y:
g(x)<g(y)
f(i)<f(i+1)
i.Unfold `increasing` i THEN BackThru i)
