At:
pred mng2 unprime211
1.
p: Fmla
2.
ds: Collection(dec())
3.
daa: Collection(dec())
4.
da: Collection(SimpleType)
5.
de: sig()
6.
rho: Decl
7.
e: {[[de]] rho}
8.
s: {[[ds]] rho}
9.
s': {[[ds]] rho}
10.
a: [[da]] rho
11.
tr: trace_env([[daa]] rho)
12.
trace_consistent_pred(rho;daa;tr.proj;p)
13.
tc_pred(p;ds;da;de)
14.
r:rel(). r p [[r]] rho ds da de e s a tr
15.
r: rel()
16.
r@0: rel()
17.
r@0 p
18.
r = rel_unprime(r@0)
19.
[[r@0]] rho ds da de e s a tr
rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr) ~ [[r@0]] rho ds da de e s a tr
By:
HypSubstSq -2 0
THEN
BackThru
Thm*r:rel(), rho,ds,da,de,e,s,s',a,tr:Top. rel_mng_2(rel_unprime(r); rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s a tr
Generated subgoals:
r:rel(). r 
p 
[[r]] rho ds da de e s a tr
rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr) ~ [[r@0]] rho ds da de e s a tr