1. p : IdLnk List
2. i : ||p||
3. j : (i+1)
4. lpath(p)
5. i-j = 0
  source(p[i]) = destination(last(l_interval(p;j;i)))

By:	RWO Thm* l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)] 0

1

source(p[i]) = destination(p[(i-1)])

2 steps

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