Thms
grammar
1
Sections
AutomataTheory
Doc
tl
Def
tl(l) == Case of l; nil
nil ; h.t
t
Thm*
A:Type, l:A*. tl(l)
A*
About:
nil ; h.t t
A:Type, l:A*. tl(l) 
A* nil ; h.t t
