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

is mentioned by

Thm* L1,L2,L:T List, x:T. Thm* no_repeats(T;L)  L1 @ [x]  L  [x / L2]  L  L1 @ [x / L2]  L	[append_overlapping_sublists]
Thm* L_1,L_2:T List. L_1  L_2  L_1  L_2	[iseg_is_sublist]
Thm* x:T, L:T List. (x  L)  [x]  L	[member_iff_sublist]
Thm* L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L	[sublist_pair]
Thm* L1,L2:T List. null(L2)  L1  tl(L2)  L1  L2	[sublist_tl]
Thm* L:T List. L  nil  L = nil	[sublist_nil]
Thm* L1,L2:T List. L1 = L2  L1  L2	[sublist_weakening]
Thm* x1,x2:T, L1,L2:T List. Thm* [x1 / L1]  [x2 / L2]  x1 = x2 & L1  L2  [x1 / L1]  L2	[cons_sublist_cons]
Thm* L:T List. nil  L  True	[nil_sublist]
Thm* L1,L2:T List. L1  L2  L2  L1  L1 = L2	[sublist_antisymmetry]
Thm* L1,L2:T List. L1  L2  ||L1|| = ||L2||    L1 = L2	[proper_sublist_length]
Thm* x:T, L:T List. [x / L]  nil  False	[cons_sublist_nil]
Thm* L1,L2:T List. L1  L2  ||L1||||L2||	[length_sublist]
Thm* L1,L2,L3:T List. L1  L2  L2  L3  L1  L3	[sublist_transitivity]
Def x before y  l == [x; y]  l	[l_before]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html