Nuprl - Proof: select-map 2 1 2

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

1. f : Top
2. T : Type
3. T List
4. T
5. v : T List
6.

||v||. map(f;v)[i] ~ (f(v[i]))
7. i :

(||v||+1)
8.

i = 0
9. 0<i

hd(nth_tl(i-1;map(f;v))) ~ (f(hd(nth_tl(i-1;v))))

By:	Fold `select` 0 THEN BackThruSomeHyp

Generated subgoals:

None

About:

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