Nuprl - Proof: map select 1 2

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

1. A : Type
2. B : Type
3. f : A

B
4. A List
5. u : A
6. v : A List
7.

||v||. map(f;v)[n] = f(v[n])
8. n :

(||v||+1)

(f(u).map(f;v))[n] = f((u.v)[n])

By:	Decide (n = 0)

Generated subgoals:

1 9. n = 0
(f(u).map(f;v))[n] = f((u.v)[n])
1 step

2 9. n = 0
(f(u).map(f;v))[n] = f((u.v)[n])
1 step

About:

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

1	9. n = 0 (f(u).map(f;v))[n] = f((u.v)[n])	1 step
2	9. n = 0 (f(u).map(f;v))[n] = f((u.v)[n])	1 step