1. T : Type
2. T' : Type
3. a : T List
4. x : T'
5. f : TT'
6. y:T. (i:. i<||a|| & y = a[i]) & x = f(y)
  i:. i<||map(f;a)|| & x = map(f;a)[i]

1

6. y : T 7. i :  8. i<||a|| 9. y = a[i] 10. x = f(y)   x = map(f;a)[i]

2 steps

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