Natural Deduction with identity: two distinct elements proof

Question

Here's an argument that's quite clearly valid, but which I'm having trouble proving in Natural Deduction:

$\exists x~\exists y~\lnot x=y \vdash\forall x~\exists y~\lnot x=y$

The informal reasoning: the premise is that there are at least two distinct elements; this implies that for every element, there is at least one element which is distinct from it.

I presume the proof will end (and I'm using what I believe is called a proof tree):

$$\exists y~\lnot a=y\over\forall x~\exists y~\lnot x=y$$

with the top sentence following from an application of negation elimination or from $\lnot a=b$ (or some constant). But after hours of trying I haven't been able to complete a proof. Can someone advise me?

Answer 1

Here's a proof in Fitch ... you can probably convert it to a proof in your system:

Answer 2

Proof sketch

1) $∃x ∃y \ ¬(x=y)$ --- premise

2) $¬∀x ∃y \ ¬(x=y)$ --- assumed [a]

3) $¬(a=b)$ --- from 1) by two $∃$-elim

4) $∃x ∀y \ (x=y)$ --- from 2) by equivalences: to be derived

5) $∀y \ (c=y)$ --- from 4) by $∃$-elim

6) $c=a$ --- from 5)

7) $c=b$ --- from 5)

8) $a=b$ --- from 6) and 7) by transitivity of equality

9) $\bot$ --- from 2) and 8)

Now we can close all the $∃$-elim's, because there are no free variables in 9). Thus:

$∀x ∃y \ ¬ (x=y)$ --- from 2) by Double Negation [that is not intuitionistically valid; see also @Max New's comment], discharging [a].