At:
rel mng wf closed
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)
13.
[[r]] rho ds < > de e s 
tr 
Prop
[[r]] rho ds da1 de e s tr Prop
By:
All (Unfold `rel_mng`)
THEN
Trivial
Generated subgoals:
None
About:
