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
  (u.v)[(j-j)] = u

By:	RWH (LemmaC Thm* a:T, as:T List, i:. i0  (a.as)[i] = a) 0

None

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