At:
pred mng 2 wf closed
1
2
2
1
3
1
1
1
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.
r:rel(). r 
p 
tc(r;ds;da;de)
13.
closed_pred(p)
14.
r: rel()
15.
r p
16.
tc(r;ds;da;de)
closed_rel(r)
By:
AllHyps (Unfold `closed_pred`)
THEN
SmAuto
Generated subgoals:
None
About:
