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

At: decls mng monotone 1 2
1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. r: l:Label[[ds1]] rho(l)
5. ds2 ds1
6. x1: Label

[[ds1]] rho LabelType
By: Fold `decl` 0
Generated subgoals:

None

About:
applyfunctionuniversemember

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