1. 'a : Type
2. 'b : Type
3. 'c : Type
4. f : 'a'b'c
5. 'a List
6. u : 'a
7. v : 'a List
8. l2:'b List. map2(f;v;l2)  'c List
9. 'b List
10. u1 : 'b
11. v1 : 'b List
12. map2(f;cons(u; v);v1)  'c List
  map2(f;cons(u; v);cons(u1; v1))  'c List

1

map2(f;v;v1)  'c List

1 step

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