1. l : IdLnk
2. u : IdLnk
3. v : IdLnk List
4. lpath([u / v])
5. ||[u / v]|| = 0
5. 
5. destination(l) = source(hd([u / v])) & hd([u / v]) = lnk-inv(l)
  lpath([l; u / v])

1

5. destination(l) = source(u) 6. u = lnk-inv(l)  IdLnk   lpath([l; u / v])

3 steps

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