1. T : Type
2. T' : Type
3. f : TT'
4. T List
5. T
6. v : T List
7. x',y':T'.
7. x' before y'  map(f;v)  (x,y:T. x before y  v & f(x) = x' & f(y) = y')
8. x' : T'
9. y' : T'
10. x : T
11. y : T
12. x before y  v
13. f(x) = x'
14. f(y) = y'
  x' before y'  map(f;v)

1

x,y:T. x before y  v & f(x) = x' & f(y) = y'

1 step

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