Prove or disprove: if $⊢_{FOL}\exists x\forall y\ \psi$ then $⊢_{FOL}\psi\{t/x\}$

Question

Let $\psi$ be a formula without quantifiers in a language with at least one constant ,
such that $\exists x\forall y\ \psi$ is a sentence.
Prove or disprove:
If $⊢_{FOL}\exists x\forall y\ \psi$ then there's exist a closed term $t$ such that $⊢_{FOL}\psi\{t/x\}$

I think the claim is correct.
I tried proving it as follows:
$⊢_{FOL}\exists x\forall y\ \psi$ iff
$\forall x\exists y\ \neg\psi$ isn't satisfiable iff (by Skolem theorem)
$\forall x\ \neg\psi\{f(x)/y\}$ isn't satisfiable (where $f$ is a new function symbol)
then I tried to use Herbrand's theorem and I got stuck.

Answer 1

I've found a counter example:
Let $\sigma=\{c,p\}$
Let $\psi=p(y)\vee\neg p(x)$

So:
$\vdash_{FOL}\exists x\forall y\ (p(y)\vee\neg p(x))$)
Because $\exists x\forall y\ (p(y)\vee\neg p(x)) \equiv (\forall y \ p(y))\vee (\neg \forall x \ p(x))$

But:
$\nvdash_{FOL}p(y)\vee\neg p(c)$
Because if we define:
$M=<\{0,1\},I>$ such that $I[p]=\{1\}\ ,I[c]=1$
and an assignment $v$ such that $v[y]=0$,
then $v[p(y)\vee\neg p(c)]=$f
and $c$ is the only closed term in the language

Answer 2

Yes, this is true.

I think it is most easily seen by using sequent calculus as your proof system for first order logic.

Sequent calculus has the nice property that everything that is provable has a cut-free proof -- and the only rule a cut-free proof of $\vdash \exists x\forall y\, \psi$ can end with is $\exists$R. ...

Ha! this is not true, as shown by the OP's counterexample where $\exists x \forall y. \psi$ is the Drinker Paradox. When one writes down a proof of the Drinker Paradox and eliminates cuts, what one ends up with is a proof where the last rule is not $\exists$R, but the right contraction rule. So my entire argument collapses.

(I'll let this this answer stand as a warning for the careless ...)