PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
lremove
mem
2
1
2
1.
St:
Type
2.
l:
St*
3.
s:
St
4.
eq:
St
St
5.
sx:
St
6.
eq(s,sx)
7.
mem_f(St;sx;nil)
mem_f(St;sx;nil \ s)
By:
RecUnfold `mem_f` -1
THEN
Reduce -1
Generated subgoals:
None
About:
St
eq(s,sx)
mem_f(St;sx;nil \ s)
