L2
Def ==
f:(
||L1||
||L2||).
Def == increasing(f;||L1||) & (
j:||L1||. L1[j] = L2[(f(j))] 
T) L2
f:(||L1||||L2||).
j:||L1||. L1[j] = L2[(f(j))] T)is mentioned
In prior sections: mb list 1 mb list 2
Try larger context:
EventSystems
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html