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

At: decls mng monotone 1
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(x1)) ([[ds2]] rho(x1))
By: Unfold `subtype` 0
Generated subgoals:

17. x: [[ds1]] rho(x1)
x [[ds2]] rho(x1)
2 [[ds1]] rho LabelType

About:
applyfunctionuniversemembersubtype

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