f1:(
||L1||
||L||), f2:(||L2||||L||). increasing(f1;||L1||) & (
j:||L1||. L1[j] = L[(f1(j))] 
T) & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[(f2(j))] T) & (j1:||L1||, j2:||L2||. 
f1(j1) = f2(j2))
is mentioned
In prior sections: mb list 2