Type systems usually have the type preservation property: if a typable term beta-reduces, then the resulting term is still typable.\xa0 So typing is closed under beta-reduction.\xa0 With intersection typing, typing is also closed under beta-expansion, which is a critical step in showing that intersection typing is complete for normalizing terms: any normalizing term can be typed with intersection types (and simple function types).\xa0\xa0