1. p : IdLnk List
2. i : ||p||
3. j : (i+1)
4. lpath(p)
  lpath(l_interval(p;j;i))

By:	ParallelOp -1 THEN Inst Thm* l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j   [IdLnk;p;i;j] THEN RWO Thm* l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)] 0 THEN Reduce 0 THEN InstHyp [j+i@0] -3 THEN All ArithSimp

None

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