Nuprl - Proof: member map 1 1 1

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

1. T : Type
2. T' : Type
3. a : T List
4. x : T'
5. f : T

T'
6. i :

7. i<||a||
8. x = f(a[i])

i@0:

. i@0<||a|| & a[i] = a[i@0]

By:	InstConcl [i]

Generated subgoals:

None

About:

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