PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: firstn lem1 1 2 2 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

u.firstn(x+1-1;v) = (if 0 < x u.firstn(x-1;v) else nil fi @ [(u.v)[x]])
By: SplitOnConclITE
Generated subgoal:

110. 0 < x
u.firstn(x+1-1;v) = ((u.firstn(x-1;v)) @ [(u.v)[x]])

About:
equallistconssubtractaddnatural_numberifthenelse
niluniverseintless_thanallimplies