T:Type, L1,L2,L:T List, x:T.
  no_repeats(T;L)  L1 @ [x]  L  [x / L2]  L  L1 @ [x / L2]  L

1

1. T : Type 2. L1 : T List 3. L2 : T List 4. L : T List 5. x : T 6. i,j:. i<||L||  j<||L||  i = j  L[i] = L[j] 7. f1 : ||L1 @ [x]||||L|| 8. increasing(f1;||L1 @ [x]||) 9. j:||L1 @ [x]||. (L1 @ [x])[j] = L[(f1(j))] 10. f : (||L2||+1)||L|| 11. increasing(f;||L2||+1) 12. j:(||L2||+1). [x / L2][j] = L[(f(j))]   f:(||L1 @ [x / L2]||||L||).    increasing(f;||L1 @ [x / L2]||)   & (j:||L1 @ [x / L2]||. (L1 @ [x / L2])[j] = L[(f(j))])

40 steps

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