On skolomizing quantifiers I have a quick question on how skolomizing quantifiers. I understand the following

∀x(Something(x) -> ∃y(Else(x,y))) => ∀x(Something(x) -> (Else(x,f(x)))

What I need help understanding is what to do when it's configured like this:

∃x(Something(x) -> ∀y(Else(x,y)))

If I eliminate the existential quantifier first like what's usually done, do I put down x as f(y) or y as f(x). Do I instead start with the universal quantifier?
 A: You always first pull out all quantifiers to the front. So
$\phantom{\rightsquigarrow} \exists x (Something(x) \to \forall y (Else(x,y)))\\  
\rightsquigarrow \exists x \forall y (Something(x) \to Else(x,y))$
Then you eliminate the quantifiers from left to right, so first $\exists x$, then $\forall y$.
There are two slightly different variants of skolemization, and I don't know which variant you learnt:
The first variant eliminates universal quantifiers one by one. In that case, the skolem function for the existential quantifier is applied to all variables occurring free in the remaining formula. Usually these will be the variables left over from eliminated universal quantifiers having occurred left to the existential quantifier.
The second variant first computes the universal closure of the formula to bind all free variables, stepwise eliminates the existential quantifiers but leaves the universal ones in place for the moment, and removes the universal quantifiers all in one batch at the end. In that case, the skolem function for the existential quantifier is applied to all variables bound by universal quantifiers occurring before the existential quantifier.
In both variants, for the present case there are no variables to apply the skolem function to, because the universal quantifier only comes afterwards. So the resulting function is a 0-place function, with no arguments at all:
$\phantom{\rightsquigarrow} \exists x \forall y (Something(x) \to Else(x,y))\\
\rightsquigarrow \forall y (Something(f()) \to Else(f(),y))$
Zero-place functions behave like individual constants, and depending on the preferred notation conventions, you can also write $a$ instead of $f()$.
Then you eliminate the universal quantifier:
$\phantom{\rightsquigarrow} \forall y (Something(f()) \to Else(f(),y))\\
\rightsquigarrow Something(f()) \to Else(f(),y)$
And you're done.
The skolem function never contains the bound variable being eliminated, only the ones on which the existential quantifier is dependent, "dependent" in the sense of bound left of the existential quantifier or free, and also no variables bound after (right of) the existential quantifier.
