1. T : Type
2. n : 
3. 0<n
4. as:T List. n-1||as||  (i:(n-1). firstn(n-1;as)[i] = as[i])
5. 0<n
  as:T List. 
  n||as||
  
  (i:n. (Case of as; nil  nil ; a.as'  a.firstn(n-1;as'))[i] = as[i])

1

6. T List 7. u : T 8. v : T List 9. n||v||+1 10. i : n   (u.firstn(n-1;v))[i] = (u.v)[i]

4 steps

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