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

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

w [[da]] rho(k)
By: Unfold `decls_mng` 0
Generated subgoal:

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

About:
setapplymember

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