PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: whole segment 1

1. T: Type
2. as: T*

(as[0..||as||]) = as

By:
Unfold `segment` 0
THEN
ArithSimp 0


Generated subgoal:

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


About:
equallistnatural_numberuniverse