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

At: decls mng functionality sigma 1 1 1
1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. l: Label
5. r1: [[ds1]] rho(l)
6. ds1 = ds2

r1 [[ds2]] rho(l)
By: Using [`ds1',ds1] (BackThru Thm* ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x). (d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x))
Generated subgoal:

17. d: dec()
8. d ds2
9. d.lbl = l
d ds1

About:
applymember

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