At:
pred mng2 addprime
2
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)
trace_consistent_pred(rho;daa;tr.proj;(p)')
By:
BackThru
Thm* 
da:Collection(dec()), P:Fmla, rho:Decl, te:(Label
Label
). trace_consistent_pred(rho;da;te;P) 
trace_consistent_pred(rho;da;te;(P)')
Generated subgoals:
None
