Def L1  L2
Def == f:(||L1||||L2||). 
Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)

is mentioned

In prior sections: mb list 1 mb list 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html