(26steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: no repeats iff
  T:Type, l:T List. no_repeats(T;l)  (x,y:T. x before y  l  x = y)
By: Unfolds [`no_repeats`;`l_before`] 0 THEN Unfold `sublist` 0

Generated subgoals:

1 1. T : Type
2. l : T List
3. i,j:. i<||l||  j<||l||  i = j  l[i] = l[j]
4. x : T
5. y : T
6. f:(||[x; y]||||l||). 
6. increasing(f;||[x; y]||) & (j:||[x; y]||. [x; y][j] = l[(f(j))])
  x = y
6 steps
2 1. T : Type
2. l : T List
3. x,y:T.
3. (f:(||[x; y]||||l||). 
3. (increasing(f;||[x; y]||) & (j:||[x; y]||. [x; y][j] = l[(f(j))]))
3. 
3. x = y
4. i : 
5. j : 
6. i<||l||
7. j<||l||
8. i = j
  l[i] = l[j]
19 steps

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

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