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?