Is the statement $(\exists x\psi(x)\rightarrow\forall x\theta(x))\vdash \forall x(\psi(x)\rightarrow\theta(x))$ true in intuitionistic/minimal logic?

Question

I know that this sequent is true for classical logic. But is it true in minimal or intuitionistic logic?

What would be a Kripke model that doesn't satisfy the property?

I would appreciate some (as many as possible) Kripke model examples where classically true formulas are false.

I already have one where $\forall x\neg\phi\lor\neg\neg\phi$ is not true:

Here we have $\alpha\nvDash \neg P(a)\lor\neg\neg P(a)$

Answer 1

Yes, it is.

We can prove it without LEM or Double Negation.

1) $∃xψ(x) → ∀xθ(x)$ --- premise

2) $ψ(a)$ --- assumed [a]

3) $∃xψ(x)$ --- from 2) by $\exists$-I

4) $∀xθ(x)$ --- from 3) and 1)

5) $θ(a)$ --- from 4)

6) $ψ(a)→θ(a)$ --- from 1) and 5) by $\to$-I, discharging [a]

$∀x(ψ(x)→θ(x))$ --- from 7) by $\forall$-I.