Closed-term witness property for quantifier-free existential sentences

In a first-order language having at least one closed term, validity of a quantifier-free existential sentence forces inconsistency of the set of negations of all its closed-term instances. Otherwise take a model of those negations and its substructure generated by the closed terms. Quantifier-free truth is preserved there, so the valid existential sentence has a closed-term witness, a contradiction. Compactness then gives a finite disjunction of instances. The nonempty closed-term hypothesis is essential: in a language with no constants or nullary functions, the valid sentence $\exists x(x=x)$ has no closed-term instance.