On polymorphic types of untyped terms

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,b$a,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.