PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: add action mem 3 1
1. St: Type
2. l: St*
3. f: StSt
4. s: St
5. s': St
6. f(s') = s

mem_f(St;s';nil) mem_f(St;s;(+f)(nil))
By:
RecUnfold `mem_f` 0
THEN
Reduce 0
Generated subgoals:

None

About:
impliesniluniverselistfunctionequalapply