Can in polymorphic lambda calculus two terms have identical normal forms if we assume that set of their possible types does not intersect?

39 Views Asked by At

Let us assume, that we have context $\Gamma$ and two terms $M_1$ and $M_2$ in polymorphic lambda calculus. Let us also assume, that intersection of their possible types in context $\Gamma$ is empty(we assume that both of these terms can be typed). Is it possible for their normal forms to be identical?