I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it.
Some prelimary definitions.
A Henkin structure $A = (A^\cdot, ⟦\cdot⟧_A)$ for the simply typed $\lambda$-calculus with a single base type $o$ consists of a set $A^\sigma$ for each type $\sigma$ such that $A^{\sigma\to\tau}\subseteq (A^\tau)^{A^\sigma}$, $⟦\cdot⟧$ is a function mapping assignments and simply typed $\lambda$-term to elements of the appropriate domains satisfying the usual clauses: $⟦x⟧^g=g(x)$, $⟦\lambda x.M⟧^g = a \mapsto ⟦M⟧^{g[a/x]}$, $⟦MN⟧=⟦M⟧⟦N⟧)$.
A homomorphism between structures $A$ and $B$ is a type-indexed family of functions $h^\sigma:A^\sigma \to B^\sigma$, such that $h^\sigma(⟦ M⟧_A^g)=⟦ M⟧_B^{h\circ g}$ for every term $M$ of type $\sigma$.
An element $d\in A^\sigma$ is $\lambda$-definable iff $d = ⟦M⟧_A$ for some closed term $M$, and is $\lambda$-definable from elements $a_1...a_n$ of the structure if $d = ⟦M⟧(a_1)...(a_n)$ for some closed term $M$.
QUESTION: is it true that if $A$ is a Henkin model with $A^o$ infinite, and $d\in A^\sigma$ is an element of that is preserved by homomorphisms, in the sense that for every $h,h':A\to B$, $h^\sigma(d)=h'^\sigma(d)$, then $d$ is $\lambda$-definable?
(There are analogous questions for more general classes of models of the simply typed $\lambda$-calculus, that I would also be interested to know about if the answer depends on the type of model.)
