  We introduce a new representation of non-idempotent intersection types, using
sequences (families indexed with natural numbers) instead of lists or
multisets. This allows scaling up intersection type theory to the infinitary
lambda-calculus. We thus characterize hereditary head normalization (Klop's
Problem) and we give a unique type to all hereditary permutators (TLCA Problem
#20), which is not possible in a finite system. On our way, we use
non-idempotent intersection to retrieve some well-known results on infinitary
terms. This paper begins with a gentle, high-level introduction to intersection
type theory and to the infinitary calculus.
