1. 'a : S
2. 'a List
3. u : 'a
4. v : 'a List
5. n:. n<||v||  el(n,v) = v[n]
6. n : 
7. n<||v||+1
8. n = 0
  el(n-1,v) = cons(u; v)[n]

By:	LemmaRW Thm* a:T, as:T List, i:. 0<i  i||as||  cons(a; as)[i] = as[(i-1)] THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

1	el(n-1,v) = el(n-1,v)	1 step
2	el(n-1,v) = v[(n-1)]	1 step

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