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)
8. l : T List
9. ||l|| = n
  Q(l)

By:	Inst Thm* L:T List. 0<||L||  (x:T, L':T List. L = (L' @ [x])) [T;l] THEN ExRepD THEN MoveToConcl -4 THEN HypSubst -1 0

1

9. x : T 10. L' : T List 11. l = (L' @ [x])   ||L' @ [x]|| = n    Q(L' @ [x])

3 steps

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