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

At: sigma decls mng functionality 1 1 1
1. d1: Collection(dec())
2. d2: Collection(dec())
3. rho: Decl
4. l: Label
5. u1: [[d1]] rho(l)
6. d1 = d2
7. x: SimpleType
8. x dec_lookup(d2;l)

mk_dec(l, x) d1
By: RW (SweepDnC (RevHypC -3)) -1
Generated subgoal:

18. x dec_lookup(d1;l)
mk_dec(l, x) d1

About:
apply

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