Q:

Predicate Logic

How do I derive this?
Pr 1     ∀x(Fx -> ∀xGx)
∴        ∀x(Fx -> ∀x(Gx \ / Hx))
My attempt:

However I cannot used universal derivation due to the free x. I think using ass id and qn would be better option but I am unsure how to edit my proof so that I get the completed one. 
I am using Elogic and this is list of rules:

A:

If we rewrite the argument to avoid a clash of variables, one possible proof would be:

