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

is mentioned by

Thm* f:(AB), L1,L2:A List. L1  L2  map(f;L1)  map(f;L2)

[iseg_map]

In prior sections: mb list 1

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