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

At: decls mng functionality sigma 1
1. 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)
By: Analyze -2
Generated subgoal:

14. l: Label
5. r1: decl_type([[ds1]] rho;l)
6. ds1 = ds2
r1 decl_type([[ds2]] rho;l)

About:
productmember

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