At:
pred mng functionality
1
1
1.
p1: Collection(rel())
2.
p2: Collection(rel())
3.
ds1: Collection(dec())
4.
ds2: Collection(dec())
5.
daa: Collection(dec())
6.
da1: Collection(SimpleType)
7.
da2: Collection(SimpleType)
8.
de: sig()
9.
rho: Decl
10.
e: {[[de]] rho}
11.
s: {[[ds1]] rho}
12.
a: [[da1]] rho
13.
tr: trace_env([[daa]] rho)
14.
(
r
p1.trace_consistent_rel(rho;daa;tr.proj;r))
15.
r:rel(). r p1 
tc(r;ds1;da1;de)
16.
p1 = p2
17.
ds1 = ds2
18.
da1 = da2
s {[[ds2]] rho}
By:
Using [`ds1',ds1]
(BackThru
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds1 = ds2 r {[[ds2]] rho})
Generated subgoals:
None
About:
