At:
ioa all mng state
1
1
1
2
1.
I: Type
2.
A: I
ioa{i:l}()
3.
rho: Decl
4.
de: sig()
5.
e: {[[de]] rho}
6.
s: l:Labeldecl_type([[ioa_all(I; i.A(i)).ds]] rho;l)
7.
i: I
8.
x1: Label
[[ioa_all(I; i.A(i)).ds]] rho 
LabelType
By:
Fold `decl` 0
Generated subgoals:
None
About:
