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

is mentioned by

Thm* l:T List, x,y,z:T. Thm* no_repeats(T;l)  x before y  l  y before z  l  x before z  l	[l_before_transitivity]
Thm* l:T List. no_repeats(T;l)  (x,y:T. x before y  l  x = y)	[no_repeats_iff]
Thm* l:T List, a,x,y:T. Thm* x before y  [a / l]  x = a & (y  l)  x before y  l	[cons_before]
Thm* L:T List, a,b:T. a before b  L  (a  L)	[l_before_member2]
Thm* x,y:T. x before y  nil  False	[nil_before]
Thm* L:T List, a,b:T. a before b  L  (b  L)	[l_before_member]
Thm* x,y:T, L:T List. Thm* (x  L)  (y  L)  x = y  x before y  L  y before x  L	[l_tricotomy]

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