Working on P.D. Magnus. "forallX: an Introduction to Formal Logic" (p. 297, exercise C. 1):
$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\X#1{\qquad\mathbf{X} \: #1 \\} $ $ \fitch{1.\, \forall xA(x) \to B}{ \fitch{2.\,\neg\exists x(A(x) \to B)}{ \fitch{3.\, A(a)}{ \fitch{4.\, \neg \forall xA(x)}{ \fitch{5.\, \neg A(a)}{ 6.\, \bot \ne{3,5} }\\ 7.\, A(a) \IP{5-6} 8.\, \forall xA(x) \Ai{7} 9.\, \bot \ne{4,8} }\\ 10.\, \forall xA(x) \IP{4-9} 11.\, B \ie{1,10} }\\ 12.\, A(a) \to B \ii{3-11} 13.\, \exists x(A(x) \to B) \Ei{12} 14.\, \bot \ne{2,13} }\\ 15.\, \exists x(A(x) \to B) \IP{2-14} } $
I am not sure about my use of $\mathbf{\forall I}$ rule on line 7. $A(a)$ is discharged on line 8, but a appears in an open assumption on line 3. Is this proof correct ?
EDIT:
From @Graham Kemp answer, I modified the proof to reach this one:
$ \fitch{1.\, \forall xA(x) \to B}{ \fitch{2.\, \neg \exists x(A(x) \to B)}{ \fitch{3.\, A(b)}{ \fitch{4.\, \neg A(a)}{ \fitch{5.\, A(a)}{ 6.\, \bot \ne{4,5} 7.\, B \X{6} }\\ 8.\, A(a) \to B \ii{5-7} 9.\, \exists x(A(x) \to B) \Ei{8} 10.\, \bot \ne{2,9} }\\ 11.\, A(a) \IP{4-10} 12.\, \forall xA(x) \Ai{} 13.\, B \ie{1,12} }\\ 14.\, A(b) \to B \ii{3-13} 15.\, \exists x(A(x) \to B) \Ei{14} 16.\, \bot \ne{2,15} }\\ 17.\, \exists x(A(x) \to B) \IP{2-16} } $
You are quite correct; that is invalid.
Try building the proof with these assumptions. $$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~\forall x~A(x)\to B}{\fitch{~~2.~\neg\exists x~(A(x)\to B)}{\fitch{~~3.~A(b)}{\fitch{~~4.~\neg A(a)}{\fitch{~~5.~A(a)}{~~\vdots}\\~~\vdots}\\~~\vdots}\\~~\vdots}\\~~~.~\exists x~(A(x)\to B)}$$