Def x before y  l == [x; y]  l

is mentioned by

Thm* f:(TT'), L:T List, x',y':T'. Thm* x' before y'  map(f;L)  (x,y:T. x before y  L & f(x) = x' & f(y) = y')	[before-map]
Thm* n:, x,y:n. x before y  upto(n)  x<y	[before-upto]

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