Expression Types Continued
	• Elimination rule (destructor) D ; G |- M : �A      D,u::A ; G |- N : C D ; G |- (let box u = M in N) : C • Operational semantics captures staging                                M Þ box E    [E/u] N Þ V box E Þ box E        let box u = M in N Þ V