At:
rel mng wf closed
1
1
2
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)
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
