Nuprl - Proof: select-map 2

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

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)

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

By:	CaseNat 0 `i' THEN Reduce 0 THEN Try Trivial

Generated subgoal:

1 8. i = 0
[(f(u)) / map(f;v)][i] ~ (f([u / v][i]))
3 steps

About:

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