At:
rel mng wf closed
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)
[[r]] rho ds < > de e s 
tr 
Prop
By:
Auto
Generated subgoals:
| 1 | [[ < > ]] rho |
| 2 | tc(r;ds; < > ;de) |
About:
