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

At: sigma decls mng value 1 1
1. ds: Collection(dec())
2. rho: Decl
3. l: Label
4. a1: [[ds]] rho(l)
5. x: SimpleType
6. x dec_lookup(ds;l)

a1 [[x]] rho
By: Using [`ds',ds;`x',l] (BackThru Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x) , a:SimpleType. mk_dec(x, a) ds y [[a]] rho)
Generated subgoal:

1 mk_dec(l, x) ds

About:
applymember

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