Solution (source code)

= Solution

A <1-embedding>, or <existential embedding>, is a <structure embedding> $\alpha:A\to B$ satisfying
$$
A\models\exists\mathbf y\,\theta(\mathbf a,\mathbf y)
\quad\Longleftrightarrow\quad
B\models\exists\mathbf y\,\theta(\alpha\mathbf a,\mathbf y)
$$
for every quantifier-free $\theta$ and every parameter tuple $\mathbf a$ from $A$. The forward direction is automatic for an embedding; reflection of <existential formulas> is the extra property. For an inclusion this says that $A$ is <simply closed> in $B$. This is weaker than requiring an <elementary embedding>, which preserves all formulas.