On polymorphic types of untyped terms

•We assign polymorphic types to normal untyped lambda terms.•As a consequence we obtain various extensions of Böhm's theorem.•A better description can be found in the abstract.

Let S be a finite set of β normal closed terms and M and N a pair of β normal, η   distinct, closed terms. Then there exist polymorphic types a,ba,b such that every member of S can be typed as a, and M and N have η expansions which can be typed as b; where, in the resulting typings, the members of S can be simultaneously consistently identified, and the η expansions of M and N are βη inconsistent (no model with more than one element of any type). A similar result holds in the presence of surjective pairing.