At: term typing2 1 1 1
1. ds: Collection{i}(dec())
2. daa: Collection{i}(dec())
3. da: Collection{i}(SimpleType)
4. de: sig()
5. rho: Decl{i}
6. t: Term
7. u: Term
Type{i'}
8. w: t:{v:Term| u(v) }
s,s':{[[ds]] rho}, e:{1of(sig_mng{i:l}(de; rho))}, a:SimpleType, v:[[da]] rho
, tr:trace_env([[daa]] rho).
trace_consistent(rho;daa;tr.proj;t) 
a 
term_types(ds;da;de;t) [[t]] e s s' v tr [[a]] rho
9. y1: Label
10. s: {[[ds]] rho}
11. s': {[[ds]] rho}
12. e: {1of(sig_mng{i:l}
(de; rho))}
13. a: SimpleType
14. v: [[da]] rho
15. tr: trace_env([[daa]] rho)
16. trace_consistent(rho;daa;tr.proj;trace(y1))
17. a = lbl_pr( < Trace, y1 > )
tr.y1 [[lbl_pr( < Trace, y1 > )]] rho
By: BackThru
Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label.
trace_consistent(rho;da;tr.proj;trace(y1)) tr.y1 [[lbl_pr( < Trace, y1 > )]] rho
Generated subgoals:None
About:
