At:
vcs mng wf
2
1.
vs: vc{i:l}()
Prop{i'}
2.
ds: dec()Prop{i}
3.
da: dec()Prop{i}
4.
de: sig()
5.
rho: LabelType{i}
6.
e: {sig_mng{i:l}
(de; rho)}
7.
s: {[[ds]] rho}
8.
tr: trace_env([[da]] rho)
vs 
VCs{i}
By:
Unfold `vcs` 0
THEN
Unfold `col` 0
Generated subgoals:
None
About:
