Proof for a logical truth involving quantifiers. 
Prove: $(\forall x Fx \vee \forall x Gx)\to \forall x(Fx\vee Gx)$

My attempt:
\begin{align}
1.\space & \neg\forall x(Fx\vee Gx) & \text{(Conditional Proof)}\\
2.\space & \exists x\neg(Fx\vee Gx) & \text{Quantifier Negation on line 1}\\
3.\space & \exists x(\neg Fx\wedge \neg Gx) & \text{De Morgan's on line 2}\\
& \qquad 4.\space \neg Fx\wedge \neg Gx & \text{Existential Instantiation on line 3}\\
& \qquad 5.\space  \neg Fx & \text{Simplification on line 4}\\
& \qquad 6.\space  \neg Gx & \text{Simplification on line 4}\\
& \qquad 7.\space  \exists x \neg Fx & \text{Existential Generalization on line 5}\\
& \qquad 8.\space  \neg\forall x Fx & \text{Quantifier Negation on line 7}\\
& \qquad 9.\space  \exists x \neg Gx & \text{Existential Generalization on line 6}\\
& \qquad 10.\space  \neg\forall x Gx & \text{Quantifier Negation on line 9}\\
& \qquad 11.\space \neg\forall x Fx \wedge\neg\forall x Gx & \text{Conjunction from lines 8, 10}\\
12.\space & \neg\forall x Fx \wedge\neg\forall x Gx & \text{Existential Instantiation lines 3, 4-11}\\
13.\space & \neg(\forall  xFx \vee \forall x Gx) & \text{De Morgan's on line 12}\\
14.\space & \neg\forall x(Fx\vee Gx)\rightarrow \neg(\forall Fx \vee \forall Gx) & \text{Conditional Proof on lines 1-13}\\
15.\space &\boxed{(\forall x Fx \vee \forall x Gx) \rightarrow \forall x(Fx\vee Gx)} & \text{Transposition on line 14}
\end{align}
I am mostly concerned about the Existential Instantiation subproof from 4-11. Also, it is the first time I have done this kind of proof. So, let me know of ways to improve it!
 A: Your use of "existential generalization" and "existential instantiation" seems backward. Existential instantiation is:
$$\begin{align}
\exists x \phi(x) \\
\hline
\phi(c)
\end{align}$$
For some constant $c$. And existential generalization is when you go the other way.
Also note that after existential instatiation the symbol $c$ is a constant and you should not use that one in a quantifier then. You should probably used another name than $x$ for the constant introduced by existential instantiation.
Also note that it's normally the conditional proof that would require indentation to indicate that these statements are only a consequence of an assumption. For the existential instantiation this is not as required as we only require that we can simply get rid of a constant not appearing in our formula any longer.
A: $\vdash (\forall x~Fx~\vee~\forall x~Gx)~\to~~\forall x~(Fx\vee Gx)$
...may be proven directly via disjunctive syllogism (aka disjunctive elimination):
$(\forall x~Fx~\vee~\forall x~Gx), (\forall x~Fx)~\to~\forall x~(Fx\vee Gx), (\forall x~Gx)~\to~\forall x~(Fx\vee Gx)\vdash\forall x~(Fx\vee Gx)$
Since $\vdash (\forall x~Fx)\to \forall x~(Fx\vee Gx)$ is provable by assumption, universal elimination, disjunctive introduction, conditional introduction, and universal reintroduction.   Quite similarly we have $\vdash (\forall x~Gx)\to \forall x~(Fx\vee Gx)$.
$$\begin{array}{l|l:ll} \hdashline 1 & \quad \forall x~Fx~\vee~\forall x~Gx&& \text{Assume} \\\hdashline 2 & \qquad \forall x ~Fx &1& \text{Assume }\vee\mathsf L\\\hdashline 3 & \quad\qquad Fc &2& \forall-\\ 4 & \quad\qquad Fc\vee Gc &3& \vee+ \\\hline 5 & \qquad \forall x~(Fx\vee Gx) &4& \forall + \\ \hline 6 & \quad(\forall x~Fx)\to(\forall x~(Fx\vee Gx)) &2,5& \to+ \\ \hdashline 7 & \qquad\forall x~Gx &1&\text{Assume }\vee\mathsf R \\ \hdashline 8 & \quad\qquad Gc &7& \forall -\\ 9 & \quad\qquad Fc\vee Gc &8& \vee+ \\ \hline 10& \qquad \forall x~(Fx\vee Gx) &9& \forall + \\ \hline 11& \quad(\forall x~Gx)\to \forall x~(Fx\vee Gx) &7,10& \to+\\ \hline 12& (\forall ~Fx~\vee~\forall x~Gx)\to \forall x~(Fx\vee Gx) &1,6,11& \vee-\end{array}$$
A: Here is a proof using a Fitch-style proof checker to make sure I am applying the rules correctly:

Note that I consider both cases of the disjunction in line 1 and arrive at the same result on lines 4 and 7. Then I use disjunction elimination on line 8 and finally universal introduction on line 9.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
