At:
pred mng 2 wf closed
1
2
2
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.
tc_pred(p;ds;da;de)
13.
closed_pred(p)
14.
r: rel()
15.
r 
p
[[ < > ]] rho
By:
BackThru
Thm* 
v:Top, rho:Decl. v [[ < > ]] rho
Generated subgoals:
None
About:
