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