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
  u = cons(u; v)[n]

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

None

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