Intersection and Union Types for X

In this paper we will define a notion of sequent-style intersection type assignment on X that needs union types, and show that this notion is closed for both subject-reduction and subject-expansion. We will also show that it is an extension of the Strict system for lc.