I agree with your first symbolization :
because it seems more "natural" to assume that "leprechaun" denotes a species and not an individual; in fact, you are saying : "leprechauns exist".
But in this way we cannot prove anything; the standard semantics for first-order logic assumes that any interpretation has a not empty domain M.
This means that the formula (∃x)(x=x) is valid.
The semantics requires also that to each n-place predicate symbol P an n-ary relation P* on the domain, i.e. a set of n-tuples of members of the domain; for n=1, this must be a subset of the domain.
But nothing prevents that the said subset is the empty set; thus we cannot prove that "leprechauns exist".
Things are different if we use an individual constant l; in this case we can prove, starting from the equality axiom : x=x, the formula :
in this case, we are consistent with the semantical specifications, because for each constant symbol c, the interpretation specifies a member c* of the domain M.
This means that, having and individual constant in our language, amounts to assuming that this symbol is a name denotong an object of the domain, and thus assuming the existence of the said object.