Prove in $NI$ that $\neg\neg\exists x\forall y[P(y) \to P(x)]$

Question

I have been tasked to prove a slightly different version of the Drinker's paradox:

$\vdash_{NI} \neg\neg\exists x\forall y[P(y) \to P(x)]$

Where ${NI}$ stands for natural deduction in intuitionistic logic. My professor dubbed this the detective's paradox: "There is someone, who, if someone did murder, is the murderer"

I know that I should be looking for a statement $\varphi$ such that $$\varphi\to\exists x\forall y[P(y) \to P(x)] \land \neg\varphi\to\exists x\forall y[P(y) \to P(x)]$$

If I have this, then I may conclude \begin{align*}\varphi \lor \neg\varphi &\to \exists x\forall y[P(y) \to P(x)]\\ \neg\neg(\varphi \lor \neg\varphi) &\to \neg\neg\exists x\forall y[P(y) \to P(x)]\\ &\neg\neg\exists x\forall y[P(y) \to P(x)]\end{align*}

But I am having struggles looking for this $\varphi$. Currently I have tried $\exists x [P(x)], \forall x [P(x)]$ and many statements which use the previous two + various connectives. I am asking for a hint in the right direction so I know where to search for such $\varphi$ (or give another method for solving this in an easier way).

Edit: From the comments by Lereau and DanielIV I have tried the following:

1. Assume $\forall x [\neg P(x)]$
2. Assume $P(y)$
3. From 1, conclude $\neg P(y)$
4. From 2 and 3, conclude $\bot$
5. From ex falso quodlibet, conclude $P(x)$
6. $\to$-introduction, conclude $P(y) \to P(x)$
7. $\forall$-introduction, conclude $\forall y[P(y) \to P(x)]$
8. $\exists$-introduction, conclude $\exists x\forall y[P(y) \to P(x)]$
9. $\to$-introduction, conclude $\forall x [\neg P(x)]\to\exists x\forall y[P(y) \to P(x)]$

This is the closest I can get to a proof. Nevertheless, do I think this is invalid because the $\forall$-introduction is, in my opinion, not allowed since an assumption is made about $y$, namely $\neg P(y)$. Thus how can I correct this proof?