(9steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: sigma decls mng2 1 1 1
1. da: Collection(dec())
2. rho: Decl
3. k: Label
4. w: [[dec_lookup(da;k)]] rho

w [[d]] rho for d {d:dec()| d da }(k)
By:
Unfold `dall` 0
THEN
Reduce 0
Generated subgoal:

1 w (d:{d:dec()| d da }. [[d]] rho(k))

About:
setisectapplymember

(9steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc