I think that I need to assume $¬∀x ¬P(x)$ and then do a proof by contradiction but I am not sure if that is correct or how to go about it.
We need contradiction in the proof (but it is not a poof by contradiction) :
1) $\lnot \exists x \ Px$ --- premise
2) $\quad\quad| \quad Px$ --- assumed [a]
3) $\quad\quad| \quad \exists x \ Px$ --- from 2) by $\exists$-intro
4) $\quad\quad| \quad\bot$ --- contradiction! from 1) and 3)
5) $\lnot Px$ --- from 2)-4) by $\lnot$-intro, discharging [a]
6) $\forall x \ \lnot Px$ --- from 5) by $\forall$-intro.
We have for any proposition $Q$ not containing $x$ free, $(\exists x.P(x))\to Q\vdash \forall x.(P(x)\to Q)$. This is constructively true. Assume $P(c)$ for some arbitrary $c$, then use modus ponens on the assumption after introducing an existential, then generalize as $c$ is arbitrary. As a lambda term, it is basically currying. If you choose $Q\equiv\bot$, you get your statement using the fact that (even constructively) $\neg P\equiv P\to \bot$.