Def l1  l2 == l:T List. l2 = (l1 @ l)

is mentioned by

Thm* L_1,L_2:T List. L_1  L_2  L_1  L_2	[iseg_is_sublist]
Thm* l1,l2:T List. l1  l2  ||l1||||l2||	[iseg_length]
Thm* P:(T), L2,L1:T List. L1  L2  filter(P;L1)  filter(P;L2)	[filter_iseg]
Thm* L:T List. L  nil  null(L)	[iseg_nil]
Thm* l1,l2:T List, x:T. l1  l2  (x  l1)  (x  l2)	[iseg_member]
Thm* l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])	[iseg_select]
Thm* l:T List. nil  l	[nil_iseg]
Thm* l:T List. l  l	[iseg_weakening]
Thm* l1,l2,l3:T List. l2  l3  l1  l2  l1  l3	[iseg_transitivity2]
Thm* L1,L2:T List. L1  L2  (n:(||L2||+1). L1 = firstn(n;L2))	[firstn_is_iseg]
Thm* l1,l2,l3:T List. l1  l2  l1  l2 @ l3	[iseg_append]
Thm* l1,l2,l3:T List. l1  l2  l2  l3  l1  l3	[iseg_transitivity]
Thm* a,b:T, l1,l2:T List. [a / l1]  [b / l2]  a = b & l1  l2	[cons_iseg]

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