Intersection-Type Equations Preserving Normalization

Let $E$ be a finite set of equations between intersection types, and let $=_E$ be the congruence generated by $E$. Extend intersection-type assignment with the conversion rule that permits replacement of a derived type $\tau$ by $\sigma$ whenever $\tau =_E \sigma$. Characterize exactly those finite sets $E$ for which every term typable in the extended system is strongly normalizing under $\beta$-reduction.