(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 1 1 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||
7. increasing(f;||[x; y]||)
8. j:||[x; y]||. [x; y][j] = l[(f(j))]
9. x = l[(f(0))]
10. y = l[(f(1))]
  f(0) = f(1)  
By: Unfold `increasing` -4 THEN InstHyp [0] -4

Generated subgoals:

1 7. i:(||[x; y]||-1). f(i)<f(i+1)
8. j:||[x; y]||. [x; y][j] = l[(f(j))]
9. x = l[(f(0))]
10. y = l[(f(1))]
  0<||[x; y]||-1
1 step
2 7. i:(||[x; y]||-1). f(i)<f(i+1)
8. j:||[x; y]||. [x; y][j] = l[(f(j))]
9. x = l[(f(0))]
10. y = l[(f(1))]
11. f(0)<f(0+1)
  f(0) = f(1)  
1 step

About:
listconsnilnatural_numbersubtractless_thanapply
functionuniverseequalimpliesall
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