Expression Types
A terms denoting expressions of type A
Introduction rule (constructor)
D
; |- E : A
D
;
G
|- box E : A
E depends only on expression variables!