Nuprl - Proof: select listify id 1 2

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

1. T : Type
2. n :

3. f :

T
4. i :

n
5.

j:{...n}. 0

(

i:{j..n

}. (f{j..n

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

(f{

n})[i] = f(i)

By:	(InstHyp [0;i] 5) THEN (ArithSimp -1)

Generated subgoals:

None

About:

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