PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: lshort mem 1
1. St: Type
2. l: St*
3. eq: StSt
4. x,y:St. eq(x,y) x = y
5. s: St

mem_f(St;s;nil) mem_f(St;s;LShort(nil))
By:
Analyze 0
THEN
RecUnfold `mem_f` -1
THEN
Reduce -1
Generated subgoals:

None

About:
impliesniluniverselistfunction
boolallassertapplyequal