Nuprl - Proof: member map 2 1 1

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

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

T'
6. y : T
7. i :

8. i<||a||
9. y = a[i]
10. x = f(y)

x = f(a[i])

By:	RevHypSubst -2 0

Generated subgoals:

None

About:

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