At:
pred mng 2 wf closed
1
2
2
2
1.
p: Fmla
2.
ds: Collection(dec())
3.
daa: Collection(dec())
4.
da: Collection(SimpleType)
5.
de: sig()
6.
rho: Decl
7.
e: {[[de]] rho}
8.
s: {[[ds]] rho}
9.
s': {[[ds]] rho}
10.
tr: trace_env([[daa]] rho)
11.
trace_consistent_pred(rho;daa;tr.proj;p)
12.
tc_pred(p;ds;da;de)
13.
closed_pred(p)
14.
r: rel()
15.
r 
p
16.
rel_mng_2(r; rho; ds; < > ; de; e; s; s'; 
; tr) Prop
rel_mng_2(r; rho; ds; da; de; e; s; s'; ; tr) Prop
By:
All (Unfold `rel_mng_2`)
THEN
Trivial
Generated subgoals:
None
About:
