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

At: ioa all mng action

I:Type, A:(Iioa{i:l}()), rho:Decl, de:sig(), e:{[[de]] rho}, s:([[ioa_all(I; i.A(i)).da]] rho), i:I. s [[A(i)]] rho de e.action
By: Auto
Generated subgoals:

11. I: Type
2. A: Iioa{i:l}()
3. rho: Decl
4. de: sig()
5. e: {[[de]] rho}
6. s: ([[ioa_all(I; i.A(i)).da]] rho)
7. i: I
s [[A(i)]] rho de e.action
21. 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'}

About:
functionuniversemembersubtypeall

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