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

At: decls mng subtype 1 1
1. ds: Collection(dec())
2. rho: Decl
3. x: Label
4. y: d:{d:dec()| d ds }. [[d]] rho(x)
5. a: SimpleType
6. mk_dec(x, a) ds

mk_dec(x, a) = mk_dec(x, a) {d:dec()| d ds }
By: Fold `member` 0
Generated subgoal:

1 mk_dec(x, a) {d:dec()| d ds }

About:
setisectapplyequalmember

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