Let $N$ be the standard full model of the simply typed lambda calculus with infinite base type $o$ and let $X$ be an infinite and coinfinite subset of $N(o)$. I want to know if there's a full functional submodel $M$ of $N$ such that $M\cap X=\emptyset$.

The union of any chain of functional submodels disjoint from $X$ is also a functional submodel disjoint from $X$, so by Zorn's lemma there's a maximal submodel with this property. My conjecture is that any such maximal functional submodel would be full, but I haven't been able to show this. Any pointers to relevant literature would also be welcome.

*Note on terminology*. Given some infinite set $N(o)$, $N(\cdot)$ is defined on complex types by identifying $N(\sigma\to\tau)$ with the set of all functions from $N(\sigma)$ to $N(\tau)$. Write $N$ for the union $\bigcup_\tau N(\tau)$. A submodel of $N$, as I am using the term, is a subset $M\subseteq N$ that is closed under application and contains the $S$ and $K$ combinators of $N$ (note in particular that it is not enough that a submodel merely contain and be closed under elements that behave like $S$ and $K$ relative to the submodel). Write $M(\sigma)$ for $M\cap N(\sigma)$, and interpret the application function $*: M(\sigma\to\tau) \to (M(\sigma)\to M(\tau))$ in the obvious way as the restriction of ordinary function application to $M$. Say that a submodel is additionally *functional* if $*$ is injective, and *full* if it is surjective.