Def == increasing(f;||L1||) & (
j:
||L1||. L1[j] = L2[(f(j))] 
T)j:||L1||. L1[j] = L2[(f(j))] T)is mentioned by
L:T List, n:, f:(n  ||L||).
Thm* increasing(f;n) Thm*  
Thm* (  L1:T List. ||L1|| = n  & sublist_occurence(T;L1;L;f)) | [range_sublist] |
Try larger context:
MarkB generic
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html