Herbrand disjunction for a universal theory ($T\models \exists \vec{x}\theta (\vec{x})⟹T\models {\bigvee }_{i=1}^m\theta ({\vec{t}}_i)$)

If a universal first-order theory in a first-order language with a constant entails an existential sentence with quantifier-free matrix, it entails a finite disjunction of closed-term instances of that matrix. Otherwise a first-order model of the first-order theory and all negated ground instances would have a ground-term substructure satisfying the first-order theory. An existential witness there is a tuple of closed-term values, contradicting its negated ground instance. Compactness theorem extracts finitely many instances.