Def no_repeats(T;l) == i,j:. i<||l||  j<||l||  i = j  l[i] = l[j]  T

is mentioned by

Thm* no_repeats(T;nil)	[no_repeats_nil]
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* 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:T List, x:T. no_repeats(T;[x / l])  no_repeats(T;l) & (x  l)	[no_repeats_cons]
Thm* l:T List. no_repeats(T;l)  (x,y:T. x before y  l  x = y)	[no_repeats_iff]

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