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

At: ioa all mng state 2
1. I: Type{i}
2. A: Iioa{i:l}()
3. rho: Decl{i}
4. de: sig()
5. sig_mng{i:l}(de; rho) = sig_mng{i:l}(de; rho)
6. zzz: Decl{i}Decl{i'}

Decl{i} Decl{i'}
By: Unfold `decl` 0
Generated subgoals:

None

About:
productfunctionuniverseequalsubtype

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