(7steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: no repeats cons
  T:Type, l:T List, x:T. no_repeats(T;[x / l])  no_repeats(T;l) & (x  l)
By: Unfold `no_repeats` 0 THEN Reduce 0

Generated subgoals:

1 1. T : Type
2. l : T List
3. x : T
4. i,j:. i<||l||+1  j<||l||+1  i = j  [x / l][i] = [x / l][j]
5. i : 
6. j : 
7. i<||l||
8. j<||l||
9. i = j
  l[i] = l[j]
2 steps
2 1. T : Type
2. l : T List
3. x : T
4. i,j:. i<||l||+1  j<||l||+1  i = j  [x / l][i] = [x / l][j]
  (x  l)
3 steps
3 1. T : Type
2. l : T List
3. x : T
4. i,j:. i<||l||  j<||l||  i = j  l[i] = l[j]
5. (x  l)
6. i : 
7. j : 
8. i<||l||+1
9. j<||l||+1
10. i = j
  [x / l][i] = [x / l][j]
1 step

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

(7steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc