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

At: decls mng functionality 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
THEN
Unfold `subtype` 0
THEN
UnivCD
Generated subgoal:

16. x1: Label
7. x: decl_type([[ds1]] rho;x1)
x decl_type([[ds2]] rho;x1)

About:
functionmember

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