Thms grammar 1 Sections AutomataTheory Doc

hd Def hd(l) == Case of l; nil "?" ; h.t h

Thm* A:Type, l:A*. ||l||1 hd(l) A

About:
!abstractionlist_indtokenalluniverse
listimpliesnatural_numbermember