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. x : T
10. L' : T List
11. l = (L' @ [x])
  ||L' @ [x]|| = ||L'||+1  

By:	Inst Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||   [T;L';[x]] THEN Reduce -1

None

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