At:
pred mng functionality
1
2
3
2
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
19.
s {[[ds2]] rho}
20.
r:rel(). r p2 [[r]] rho ds2 da2 de e s a tr
21.
r: rel()
22.
r p1
23.
[[r]] rho ds2 da2 de e s a tr
trace_consistent_rel(rho;daa;tr.proj;r)
By:
AllHyps (
h.(Unfold `col_all` h) THEN (BackThru h))
THEN
AllHyps (h.(Unfold `col_equal` h) THEN (BackThru h))
Generated subgoals:
None
About:
