L1,L2:T List. L1 
L2 
(
n:
(||L2||+1). L1 = firstn(n;L2))as,bs:T List. ||as @ bs|| = ||as||+||bs|| 
l:T List. ||l|| = 0 l = nilas:A List, n:{0...||as||}. ||firstn(n;as)|| = n L:T List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) = L| Theorem | Name |
| L1,L2:T List. L1 L2 (n:(||L2||+1). L1 = firstn(n;L2)) | [firstn_is_iseg] |
| cites the following: | |
| as,bs:T List. ||as @ bs|| = ||as||+||bs|| | [length_append] |
| l:T List. ||l|| = 0 l = nil | [length_zero] |
| as:A List, n:{0...||as||}. ||firstn(n;as)|| = n | [length_firstn] |
| L:T List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) = L | [append_firstn_lastn] |