1. T : Type
2. T List
3. n : 
4. u : T
5. v : T List
6. j:. j+||v|| = n  (i.v[(i-j)]){j..n} = v
7. j : 
8. j+||v||+1 = n
9. j<n
  (i.(u.v)[(i-j)]){(j+1)..n} = v

By:	RWH (LemmaC Thm* a:T, as:T List, i:. 0<i  i||as||  (a.as)[i] = as[(i-1)]) 0

1

(i.v[(i-j-1)]){(j+1)..n} = v

2 steps

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