Regular-logic separation of a proper subobject ($S\hookrightarrow A\text{ proper}⟹M(S)⊊M(A)$)

For a small category that is a regular category, use a sort for each object, an operation for each morphism, and regular theory axioms describing finite limits and regular epimorphisms. Its models are regular functors into the Category of sets. For a proper subobject $m:S\hookrightarrow A$, the sequent asserting $\forall x:A\exists y:S,m(y)=x$ cannot be derivable, since its categorical interpretation would make $m$ a cover and hence invertible. The chase completeness for regular logic supplies a model where it fails. It is essential to allow empty sorts.