Thms exponent Sections AutomataTheory Doc

length Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)

Thm* A:Type, l:A*. ||l||

Thm* ||nil||

About:
recursive_def_notice!abstractionlist_indnatural_numberaddall
universelistmemberintnil