Solution (source code)

= Solution

A <model-complete theory> is a <first-order theory> for which every <structure embedding> between two of its <first-order models> is an <elementary embedding>. Thus, if $f:\mathcal A\hookrightarrow\mathcal B$ is such an embedding, then for every <first-order formula> $\varphi(\mathbf x)$ and tuple $\mathbf a$ from $A$,
$$
\boxed{\mathcal A\models\varphi(\mathbf a)\iff\mathcal B\models\varphi(f\mathbf a).}
$$
<first-order model> completeness does not assert that every two <first-order models> are elementarily equivalent: it constrains embeddings that exist between <first-order models>, whereas completeness constrains all <first-order models>.