(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. 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 : ||[xy]||||l||
7. increasing(f;||[xy]||)
8. j:||[xy]||. [xy][j] = l[(f(j))]
9. x = l[(f(0))]
10. y = l[(f(1))]
  x = y


By: AllHyps (InstHyp [f(0);f(1)])


Generated subgoals:

1   f(0) = f(1)  
3 steps
2 11. l[(f(0))] = l[(f(1))]
  x = y

1 step

About:
listconsnilnatural_numberless_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