PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: firstn lem1 1 1 2 1 1
1. T: Type
2. as: T*
3. u: T
4. v: T*
5. 0 < ||v||+1

firstn(0;v) = nil
By:
Thin -1
THEN
ListInd 4
THEN
RecUnfold `firstn` 0
THEN
Reduce 0
Generated subgoals:

None

About:
equallistnatural_numberniluniverseless_thanadd