Proof of $\exists x \exists y (\varphi(x)\rightarrow \psi(y)) \rightarrow \exists x (\varphi(x)\rightarrow \psi(x))$ in natural deduction How to show the following trivial implication with natural deduction?

$\exists x \exists y (\varphi(x)\rightarrow \psi(y)) \rightarrow \exists x  (\varphi(x)\rightarrow \psi(x))$

Thx.
It's a conditional. So the shape of the proof, we know, is going to look like this:

$\quad\quad|\quad \exists x \exists y(\phi(x) \to \psi(y))\\
\quad\quad|\quad \ldots\\
\quad\quad|\quad \exists x(\phi(x) \to \psi(x))\\
\quad \exists x \exists y(\phi(x) \to \psi(y)) \to \exists x(\phi(x) \to \psi(x))
$

where we  use conditional proof.

If in doubt, a good strategy is to try reductio: and assuming the negation of our target in the subproof is nice as it is equivalent to a universal from which we can extract lots of info. Good! So this should work:

$\quad\quad|\quad \exists x \exists y(\phi(x) \to \psi(y))\\
\quad\quad|\quad\quad|\quad \neg\exists x(\phi(x) \to \psi(x))\\
\quad\quad|\quad\quad|\quad \forall x\neg(\phi(x) \to \psi(x))\\  
\quad\quad|\quad\quad|\quad  \ldots\\
\quad\quad|\quad\quad|\quad  \bot\\
\quad\quad|\quad \neg\neg\exists x(\phi(x) \to \psi(x))\\
\quad\quad|\quad \exists x(\phi(x) \to \psi(x))\\
\quad \exists x \exists y(\phi(x) \to \psi(x)) \to \exists x(\phi(x) \to \psi(x))
$

Right! So now we need to use the initial assumption. The only thing we can do with an existential is start off on an existential quantifier elimination proof .... so we know we need to fill in this:

$\quad\quad|\quad \exists x \exists y(\phi(x) \to \psi(y))\\
\quad\quad|\quad\quad|\quad \neg\exists x(\phi(x) \to \psi(x))\\ 
\quad\quad|\quad\quad|\quad \forall x\neg(\phi(x) \to \psi(x))\\
\quad\quad|\quad\quad|\quad\quad|\quad  \exists y(\phi(a) \to \psi(y))\\ 
\quad\quad|\quad\quad|\quad\quad|\quad   \ldots\\
\quad\quad|\quad\quad|\quad\quad|\quad \bot \\
\quad\quad|\quad\quad|\quad  \bot\\
\quad\quad|\quad \neg\neg\exists x(\phi(x) \to \psi(x))\\
\quad\quad|\quad \exists x(\phi(x) \to \psi(x))\\
\quad \exists x \exists y(\phi(x) \to \psi(y)) \to \exists x(\phi(x) \to \psi(x))
$

Do you see that the initial assumption at line 1, and the sup-proof from lines 4 to 6 entitle to the conclusion at line 7 where we discharge the temporary assumption at line 4? This is an application of existential quantifier elimination.

So how do we get from line 4 to line 6. Drat! Another existential. Same trick, then ...

$\quad\quad|\quad \exists x \exists y(\phi(x) \to \psi(y))\\
\quad\quad|\quad\quad|\quad \neg\exists x(\phi(x) \to \psi(x))\\ 
\quad\quad|\quad\quad|\quad \forall x\neg(\phi(x) \to \psi(x))\\
\quad\quad|\quad\quad|\quad\quad|\quad  \exists y(\phi(a) \to \psi(y))\\ 
\quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad  (\phi(a) \to \psi(b))\\
\quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad   \ldots\\
\quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad \bot\\ 
\quad\quad|\quad\quad|\quad\quad|\quad \bot \\
\quad\quad|\quad\quad|\quad  \bot\\
\quad\quad|\quad \neg\neg\exists x(\phi(x) \to \psi(x))\\
\quad\quad|\quad \exists x(\phi(x) \to \psi(x))\\
\quad \exists x \exists y(\phi(x) \to \psi(y)) \to \exists x(\phi(x) \to \psi(x))
$

Now, we haven't used the universal quantifier, and we have two names to instantiate it with. Do it!!

$\quad\quad|\quad \exists x \exists y(\phi(x) \to \psi(y))\\
\quad\quad|\quad\quad|\quad \neg\exists x(\phi(x) \to \psi(x))\\ 
\quad\quad|\quad\quad|\quad \forall x\neg(\phi(x) \to \psi(x))\\
\quad\quad|\quad\quad|\quad\quad|\quad  \exists y(\phi(a) \to \psi(y))\\ 
\quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad  (\phi(a) \to \psi(b))\\
\quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad  \neg(\phi(a) \to \psi(a))\\
\quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad  \neg(\phi(b) \to \psi(b))\\
\quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad   \ldots\\
\quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad \bot\\ 
\quad\quad|\quad\quad|\quad\quad|\quad \bot \\
\quad\quad|\quad\quad|\quad  \bot\\
\quad\quad|\quad \neg\neg\exists x(\phi(x) \to \psi(x))\\
\quad\quad|\quad \exists x(\phi(x) \to \psi(x))\\
\quad \exists x \exists y(\phi(x) \to \psi(y)) \to \exists x(\phi(x) \to \psi(x))
$

Ahah! The remaining bit of proof to fill in the dots is just propositional calculus reasoning. Can you do it???

And if you prefer your ND proofs laid out Gentzen style, you'll have to massage this proof idea into a spreading tree.
Using proof by contradiction:

$$\forall x \colon (\varphi (x) \wedge \neg \psi(x)$$

It follows:

$$\forall x \colon \varphi(x)$$

$$\forall x: \neg \psi(x)$$

Renaming variables:

$$\forall y \colon \neg \psi (y)$$

Using modus tollens:

$$\exists x \colon \neg \varphi(x)$$

This is a contradiction. We're done.