At:
ioa all mng action
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:Label
decl_type([[ioa_all(I; i.A(i)).da]] rho;l)
7.
i: I
8.
l: Label
[[ioa_all(I; i.A(i)).da]] rho 
LabelType
By:
Fold `decl` 0
Generated subgoals:
None
About:
