At:
closed pred mng1212
1.
p: Fmla
2.
rho: Decl
3.
ds: Collection(dec())
4.
daa: Collection(dec())
5.
da1: Collection(SimpleType)
6.
da2: Collection(SimpleType)
7.
de: sig()
8.
s: {[[ds]] rho}
9.
e: {[[de]] rho}
10.
a1: Top
11.
a2: Top
12.
tr: trace_env([[daa]] rho)
13.
trace_consistent_pred(rho;daa;tr.proj;p)
14.
tc_pred(p;ds;da1;de)
15.
closed_pred(p)
16.
r: rel()
17.
r p
[[r]] rho ds da1 de e s tr Prop
By:
BackThru
Thm*rho:Decl, ds,daa:Collection(dec()), da1:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, tr:trace_env([[daa]] rho), r:rel(). closed_rel(r) tc(r;ds;da1;de) trace_consistent_rel(rho;daa;tr.proj;r) [[r]] rho ds da1 de e s tr Prop
THEN
EasyHypThen Auto
Generated subgoals:
p
[[r]] rho ds da1 de e s 
tr 
rho:Decl, ds,daa:Collection(dec()), da1:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, tr:trace_env([[daa]] rho), r:rel(). closed_rel(r) 
tc(r;ds;da1;de)