PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: whole segment 1 1
1. T: Type
2. as: T*

firstn(||as||;nth_tl(0;as)) = as
By:
RecUnfold `nth_tl` 0
THEN
Reduce 0
Generated subgoal:

1 firstn(||as||;as) = as

About:
equallistnatural_numberuniverse