IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
increasing is id12 1. k : 2. 0<k 3. f:((k-1)(k-1)). increasing(f;k-1) (i:(k-1). f(i) = i)
4. f : kk 5. increasing(f;k)
6. k increasing(j.f(j);k-1)
By:
All (Unfold `increasing`) THEN Reduce 0 THEN BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
f:(
(k-1)
(
increasing(
j.f(j);k-1)
