(15steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: pred mng 2 wf closed 2

1. p: Fmla{i}
2. ds: Collection{i}(dec())
3. daa: Collection{i}(dec())
4. da: Collection{i}(SimpleType)
5. de: sig()
6. rho: Decl{i}
7. sig_mng{i:l}(de; rho) = sig_mng{i:l}(de; rho)
8. zzz: Decl{i}Decl{i'}

Decl{i} Decl{i'}

By: Unfold `decl` 0

Generated subgoals:

None

About:
productequalsubtype

(15steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc