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

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

< k,w > ([[da]] rho)
By:
Unfold `sigma` 0
THEN
Unfold `decl_type` 0
Generated subgoal:

1 w [[da]] rho(k)

About:
pairapplymember

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