1. T : Type
2. Q : (T List)Prop
3. Q(nil)
4. ys:T List, x:T. Q(ys)  Q(ys @ [x])
5. n : 
6. 0<n
7. l:T List. ||l|| = n-1  Q(l)
  l:T List. ||l|| = n    Q(l)

1

8. l : T List 9. ||l|| = n     Q(l)

4 steps

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