At:
pred mng functionality
1
2
4
3
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
19.
s {[[ds2]] rho}
20.
r: rel()
21.
r p2
tc(r;ds2;da2;de)
By:
Using [`ds1',ds1;`da1',da1]
(BackThru
Thm* r:rel(), ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). ds1 = ds2 da1 = da2 (tc(r;ds1;da1;de) 
tc(r;ds2;da2;de)))
Generated subgoal:
| 1 | tc(r;ds1;da1;de) |
About:
