At:
vc mng wf
2
1
1.
y: qimp{i:l}()
2.
ds: Collection(dec())
3.
da: Collection(dec())
4.
de: sig()
5.
rho: Decl
6.
e: {[[de]] rho}
7.
s: {[[ds]] rho}
8.
tr: trace_env([[da]] rho)
9.
tc_pred(y.hyp;ds;dec_lookup(da;y.lbl);de)
10.
tc_pred(y.concl;ds;dec_lookup(da;y.lbl);de)
11.
trace_consistent_pred(rho;da;tr.proj;y.hyp)
12.
trace_consistent_pred(rho;da;tr.proj;y.concl)
13.
v: [[dec_lookup(da;y.lbl)]] rho
14.
[[y.hyp]] rho ds dec_lookup(da;y.lbl) de e s v tr
< y.lbl,v > 
(
[[da]] rho)
By:
BackThruLemma'
Thm* 
da:Collection(dec()), rho:Decl, k:Label, w:[[dec_lookup(da;k)]] rho. < k,w > ([[da]] rho)
Generated subgoals:
None
About:
