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

At: sigma decls mng2 1 1 1 1 1 1 1
1. da: Collection(dec())
2. rho: Decl
3. k: Label
4. w: [[dec_lookup(da;k)]] rho
5. lbl: Label
6. d1: SimpleType
7. < lbl,d1 > da
8. k = lbl

w [[d1]] rho
By:
EqLblFwd
THEN
Using [`sts',dec_lookup(da;k)] (BackThru Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho , s:SimpleType. s sts v [[s]] rho)
Generated subgoal:

19. k = lbl
d1 dec_lookup(da;k)

About:
pairassertmember

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