IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
range sublist121 1. T : Type
2. T List
3. n : 4. f : n0
5. increasing(f;n)
increasing(f;0)
By:
Unfold `increasing` 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html