1. Top List
2. u : Top
3. v : Top List
4. n:. ||v||n  (firstn(n;v) ~ v)
  n:. ||v||+1n  (firstn(n;[u / v]) ~ [u / v])

1

5. n :  6. ||v||+1n   firstn(n;[u / v]) ~ [u / v]

4 steps

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