1. f : TopTop
2. n : 
3. 0<n
4. l:Top List. firstn(n-1;map(f;l)) ~ map(f;firstn(n-1;l))
  l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))

1	5. Top List   nil ~ nil	Trivial
2	5. Top List 6. u : Top 7. v : Top List 8. firstn(n;map(f;v)) ~ map(f;firstn(n;v))   firstn(n;[(f(u)) / map(f;v)]) ~ map(f;firstn(n;[u / v]))	4 steps

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