1. T : Type
2. T List
3. bs : T List
4. u : T
5. v : T List
6. i:||v||. (v @ bs)[i] = v[i]
7. i : (||v||+1)
8. i = 0
  (u.(v @ bs))[i] = (u.v)[i]

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

1

(v @ bs)[(i-1)] = v[(i-1)]

1 step

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