T:Type, l:T List, i:||l||, j:(i+1), x:(i-j).
  l_interval(l;j;i)[x] = l[(j+x)]

By:	Auto THEN Unfold `l_interval` 0 THEN RWO Thm* n:, f:(nT), i:n. mklist(n;f)[i] = f(i) 0 THEN Reduce 0

None

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