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

At: closed pred mng 2

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

Decl{i} Decl{i'}

By: Unfold `decl` 0

Generated subgoals:

None

About:
productequalsubtype

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