At:
pred mng2 unprime
3
1.
p: Fmla{i}
2.
ds: Collection{i}(dec())
3.
daa: Collection{i}(dec())
4.
da: Collection{i}(SimpleType)
5.
de: sig()
6.
rho: Decl{i}
7.
sig_mng{i:l}(de; rho) = sig_mng{i:l}(de; rho)
8.
zzz: Decl{i}
Decl{i'}
Decl{i} 
Decl{i'}
By:
Unfold `decl` 0
Generated subgoals:
None
About:
