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

At: decls mng functionality sigma


ds1,ds2:Collection(dec()), rho:Decl, r:([[ds1]] rho). ds1 = ds2 r ([[ds2]] rho)

By:
Unfold `sigma` 0
THEN
UnivCD


Generated subgoal:

11. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. r: l:Labeldecl_type([[ds1]] rho;l)
5. ds1 = ds2
r l:Labeldecl_type([[ds2]] rho;l)


About:
productmemberimpliesall

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