T:Type, l:T List, x,y,z:T.
  no_repeats(T;l)  x before y  l  y before z  l  x before z  l

1

1. T : Type 2. l : T List 3. x : T 4. y : T 5. z : T 6. no_repeats(T;l) 7. [x; y]  l 8. [y; z]  l   [x; z]  l

4 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html