Nuprl - Proof: select listify id 1 1 2 2

(12steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select listify id 1 1 2 2

1. T : Type
2. n :

3. f :

n

T
4. j : {...n-1}
5. 0

j+1

(

i:{(j+1)..n

}. (f{(j+1)..n

})[(i-(j+1))] = f(i))
6. 0

j
7. i : {j..n

}
8. j<n

(f(j).f{(j+1)..n

})[(i-j)] = f(i)

By:	Decide (i = j)

Generated subgoals:

1 9. i = j
(f(j).f{(j+1)..n})[(i-j)] = f(i)
2 steps

2 9. i = j
(f(j).f{(j+1)..n})[(i-j)] = f(i)
2 steps

About:

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

(12steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc