Thms nfa 1 Sections AutomataTheory Doc

tl Def tl(l) == ListInd(l;nil;h,t,v.t)

Thm* l:A*. tl(l) A*