Distinguishing pure, closed lambda terms Let $M$ be a full model of the simply typed lambda calculus, over some collection of base types, with the constraint that $|D_\sigma|\geq 2$ for each base type $\sigma$.
Let $a$ and $b$ be two closed and pure lambda terms (terms constructed from $\lambda$ and variables only -- that is, no constants) such that $[a ]_M = [b]_M$. Does it follow that $a$ and $b$ are $\beta\eta$ equivalent?
In other words, does every non-trivial model semantically distinguish between non-equivalent pure lambda terms?

If $a$ and $b$ are not $\beta\eta$-equivalent, by Bohm’s Theorem there exists a context separating them. Let's call these two new terms $A$ and $B$, with $A \neq B$. 
Since $[a]_M = [b]_M$, we have also $[A]_M = [B]_M$ by compositionality. 
Now think of the term 
"$T \equiv \lambda v .$ if $v = A$ then true else if $v = B$ then false".
So the denotation of true ($TA$) and false ($TB$) have to coincide in $M$.
Using similar conditionals you can then identify any two values in your model.
