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

At: decls mng functionality sigma 1 1
1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. l: Label
5. r1: decl_type([[ds1]] rho;l)
6. ds1 = ds2

r1 decl_type([[ds2]] rho;l)
By:
All (Unfold `decl_type`)
THEN
All Reduce
Generated subgoal:

15. r1: [[ds1]] rho(l)
6. ds1 = ds2
r1 [[ds2]] rho(l)

About:
applymember

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