Nuprl - Proof: select-map 2 1

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

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

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

(||v||+1)
8.

i = 0

[(f(u)) / map(f;v)][i] ~ (f([u / v][i]))

By:	Unfold `select` 0 THEN RecUnfold `nth_tl` 0 THEN Reduce 0 THEN SplitOnConclITE

Generated subgoals:

1 9. i0
hd([(f(u)) / map(f;v)]) ~ (f(hd([u / v])))
Auto

2 9. 0<i
hd(nth_tl(i-1;map(f;v))) ~ (f(hd(nth_tl(i-1;v))))
1 step

About:

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

1	9. i0 hd([(f(u)) / map(f;v)]) ~ (f(hd([u / v])))	Auto
2	9. 0<i hd(nth_tl(i-1;map(f;v))) ~ (f(hd(nth_tl(i-1;v))))	1 step