(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 2 1 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. i<||l||
7. x = l[i]
8. [x / l][0] = [x / l][(i+1)]
  False


By: (Reduce -1
(THEN
(RWO Thm* a:Tas:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] -1)
THEN
(ArithSimp -1)


Generated subgoals:

None

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