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

At: sigma decls mng monotone 1
1. d1: Collection(dec())
2. d2: Collection(dec())
3. rho: Decl
4. u: l:Labeldecl_type([[d1]] rho;l)
5. d2 d1
6. l: Label
7. x: [[d1]] rho(l)

x [[d2]] rho(l)
By: Using [`ds1',d1] (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:

18. d: dec()
9. d d2
10. d.lbl = l
d d1

About:
productapplymember

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