Do the steps 1-7 below constitute a valid proof of quantifier exchange? In particular I can seen no justification for line 4. McCune says that the arguments of Skolem functions should serve as place holders for the objects on which the existing object depends therefore equality substitution should not be applied to them. However, in 4 I am stating that a Skolem function $skFun(d)$ with one argument is equal to a Skolem constant $c$. I am aware that quantifier exchange is easily proven using other proof techniques such as natural deduction (see an earlier post). My reason for posting this question is that I am using an equational term rewriting system (CafeOBJ) which can easily process putative proof steps such as those below. How can I justify line 4? It seems that I was able to justify the other proof steps with a well known proof technique.
Theorem: $\DeclareMathOperator{\Likes}{Likes} (\exists y \forall x :\Likes(x,y)) \Rightarrow (\forall x \exists y :\Likes(x,y))$ \begin{align*} &\textbf{1} &&\exists y \forall x:\Likes(x,y) && \text{Assumption}\\ &\textbf{2} &&\forall x:\Likes(x,c) && \text{Existential instantiation 1}\\ &\textbf{3} &&\Likes(d,c) && \text{Universal Elimination 2}\\ &\textbf{4} &&\operatorname{skFun}(d) = c && \text{Define Skolem func equal to $c$ ???}\\ &\textbf{5} &&\Likes(d,\operatorname{skFun}(d)) && \text{Apply 4 (right-to-left) to 3}\\ &\textbf{6} &&\forall x:\Likes(x,\operatorname{skFun}(x)) && \text{Universal Instantiation}\\ &\textbf{7} &&\forall x \exists y:\Likes(x,y) && \text{Unskolemize 6}\\ \end{align*}
EDIT
My current understanding of lines 1-7 is that the cited justifications are not from natural deduction. To my knowledge, neither Skolemization nor the equation on line 4 can be justified by the rules of natural deduction. Is there a named deduction method used for these proof steps? I suppose I could justify 4 by a semantic model based argument i.e. in any model of the antecedent for any element $d$ there must exist at least one $c$.