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

1

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

1 step

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