1. l : IdLnk
2. u : IdLnk
3. v : IdLnk List
4. i:(||[u / v]||-1). 
4. destination([u / v][i]) = source([u / v][(i+1)])
4. & [u / v][(i+1)] = lnk-inv([u / v][i])
5. destination(l) = source(u)
6. u = lnk-inv(l)
7. i : (||[l; u / v]||-1)
8. i = 0
9. destination([u / v][(i-1)]) = source([u / v][(i-1+1)])
10. [u / v][(i-1+1)] = lnk-inv([u / v][(i-1)])
  destination([u / v][(i-1)]) = source([u / v][(i+1-1)])

None

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