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: