At: firstn lem1 1 2 2 1 1 1 1 1
1. T: Type
2. x: 
3. 0 < x
4. 
as:T*. x-1 < ||as|| 
firstn(x-1+1;as) = (firstn(x-1;as) @ [as[(x-1)]])
5. as: T*
6. u: T
7. v: T*
8. x < ||v||+1
9. 0 < x+1
10. 0 < x
x < ||u.v||
By: Reduce 0
Generated subgoals:None
About:
