1. 'a : S
2. h : 'a
3. t : hlist('a)
4. n : 
5. n<||t||+1
6. n = 0
7. n>0
8. n-1<||t||
  cons(h; t)[n] = t[(n-1)]  'a

By:	L 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))

None

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