At:
rel mng wf closed
1
1
1
1.
rho: Decl
2.
ds: Collection(dec())
3.
daa: Collection(dec())
4.
da1: Collection(SimpleType)
5.
de: sig()
6.
s: {[[ds]] rho}
7.
e: {[[de]] rho}
8.
tr: trace_env([[daa]] rho)
9.
r: rel()
10.
closed_rel(r)
11.
tc(r;ds;da1;de)
12.
trace_consistent_rel(rho;daa;tr.proj;r)
[[ < > ]] rho
By:
BackThru
Thm* 
v:Top, rho:Decl. v [[ < > ]] rho
Generated subgoals:
None
About:
