Q:((T List)
Prop).
Thm* Q(nil)
(ys:T List, x:T. Q(ys) Q(ys @ [x])) (zs:T List. Q(zs))l:T List. ||l|| = 0 
l = nilL:T List. 0<||L|| (
x:T, L':T List. L = (L' @ [x]))as,bs:T List. ||as @ bs|| = ||as||+||bs|| | Theorem | Name |
| Q:((T List)Prop).
Thm* Q(nil) (ys:T List, x:T. Q(ys) Q(ys @ [x])) (zs:T List. Q(zs)) | [list_append_singleton_ind] |
| cites the following: | |
| l:T List. ||l|| = 0 l = nil | [length_zero] |
| L:T List. 0<||L|| (x:T, L':T List. L = (L' @ [x])) | [list_decomp_reverse] |
| as,bs:T List. ||as @ bs|| = ||as||+||bs|| | [length_append] |