Thms
list
3
autom
Sections
AutomataTheory
Doc
lremove
Def
l \ a == Case of l; nil
nil ; h.l'
if eq(a,h)
l' \ a else h.(l' \ a) fi (recursive)
Thm*
St:Type, l:St*, s:St, eq:(St
St
). (l \ s)
St*
About:
nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi
(recursive)
St:Type, l:St*, s:St, eq:(St
St
). (l \ s) 
St* nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi
(recursive)
