What strategies could be used to prove the validity of this argument in order to not violate restrictions on universal generalization (Hurley) I'm considering a particular argument while working through Hurley's Concise Introduction:
1.  (x)(Ax -> Bx)
2.  (x)(Bx -> (E!y)Cxy)
3.  (x)(Cxy -> Dx)
/ (x)(Ax -> Dx)

I verified the validity of this argument using truth-trees.  However, moving on to actually deriving the conclusion, my current strategy is to use conditional proof:
1.  (x)(Ax -> Bx)
2.  (x)[Bx -> (E!y)Cxy]
3.  (x)(y)(Cxy -> Dx)
4.      | Ax
5.      | Bx
6.      | (E!y)Cxy
7.      | ?
8.      | Dx
9.  Ax -> Dx
10. (x)(Ax -> Dx)

My first thought would be to use existential instantiation:
1.  (x)(Ax -> Bx)
2.  (x)[Bx -> (E!y)Cxy]
3.  (x)(y)(Cxy -> Dx)
4.      | Ax
5.      | Bx
6.      | (E!y)Cxy
7.      | Cxa
8.      | Cxa -> Dx
9.      | Dx
10. Ax -> Dx
11. (x)(Ax -> Dx)

However, this seems to be a violation of the restriction on universal generalization: according to Hurley, "UG must not be used if the instantial variable [x] is free in any preceding line obtained by EI."
By the time the conditional is discharged at line 10, the instance variable x is free in a line resulting from existential instantiation, line 7.
Given that this argument is valid, what other intuitive ways might you approach this problem?  Am I misunderstanding the restriction on universal generalization?
I do want to stress that this is not an assignment.
 A: 
However, this seems to be a violation of the restriction on universal generalization: according to Hurley, "UG must not be used if the instantial variable [x] is free in any preceding line obtained by EI."

Don't be confused by their use of $[x]$.  The important issue is that whatever letter is used, it is the instantiation variable.
Here it is $a$ that is the instantiation variable.  Since this $a$ does not occur free in any line preceding the instantiation, you may use existential generalisation on anything where it occurs consequent of the instantiation.
Further, since $a$ does not even occur in the conclusory $Dx$, existential generalisation is not required.
$${\vdots\\(\forall x)(\forall y)(Cxy\to Dx)\text{ here}\\\quad{\mid\quad{Ax\hspace{34ex}\text{Assumption (arbitrary $x$ occurs free)}\\\vdots\\(\exists!y)Cyx\\(\exists y)(Cxy\wedge(\forall z)(Cxz\to z=y))\hspace{5ex}\text{A Definition of uniqueness}\\\quad{ Cx\color{red}a\wedge(\forall z)(Cxz\to z=\color{red}a)\hspace{9ex}\text{Existential Instance (witnessed by }\color{red}a)\\Cx\color{red}a\hspace{31ex}\text{Simplification}\\Cx\color{red}a\to Dx\hspace{24ex}\text{Universal Instantiation}}\\Dx\hspace{34ex}\textit{Modus Ponens}\text{ ($a$ no longer occurs)}}\\Ax\to Dx}\\(\forall x)(Ax\to Dx)}$$
[It is helpful to use indentation to identify where an instantation variable occurs, to ensure the rules are cleanly followed.  This is optional.]
