$a$ is a constant.
We want to prove that :
$(\forall xF(x))\rightarrow G(a)$ implies $\exists x(F(x)\rightarrow G(a))$
I'm working from the conclusion up to the hypotheses. The problem is I cannot get the "$\forall xF(x)$" part as an hypothesis. On line (3), I cannot instantiate it to the declared x variable (between line (1) and (2)) unfortunately. I've tried a excluded middle law with "$\forall xF(x)$" and its negation, but the negation case seems impossible to me.
The declaration blocks (Let x...) are difficult to use, too.
I think maybe I should use absurd law or excluded middle law, but I didn't suceed for some days.
The proof must be syntactic, in Fitch style. I know that $P\rightarrow Q$ is equivalent to $\neg P\lor Q$ (I think the name is material implication, but I cannot use it directly in the software), but I would like a solution using basic deduction rules and no lemma/shortcuts.
The rules I can use are described here : https://app.edukera.com/?doc=1 , I think it's natural deduction.
Please give the complete Fitch-style proof with the same rules used.
Edukera is buggy (e.g. in certain situations there's no way to cancel an application of IP), and even beyond that I find it quite unpleasant, since it won't let you introduce arbitrary subderivations in the middle of your proof (doing this would actually make this proof clearer, and the solutions proposed by the other commenters much less annoying to implement). No matter. Here's one way to derive your goal, $$((\forall x. F(x)) \rightarrow G(a)) \rightarrow \exists x. F(x) \rightarrow G(a),$$ in natural deduction.
First, notice that there are two possibilities. Either $\forall x. F(x)$, or else $\neg \forall x. F(x)$.
In the first case, modus ponens immediately lets us conclude $G(a)$, so we have $F(a) \rightarrow G(a)$, and therefore $\exists x. F(x) \rightarrow G(a)$ -- namely, $a$ constitutes such an $x$.
In the second case, we have to first prove that $\exists x. \neg F(x)$.
Now that we have $\exists x. \neg F(x)$, we just consider a $t$ such that $\neg F(t)$. Of course, for that $t$, we have $F(t) \rightarrow G(a)$, and therefore $\exists x. F(x) \rightarrow G(a)$.
After transcribing this idea into Edukera, you'll get the proof shown on the screenshot below. The first case is handled by lines 2 to 5, while $\exists x. \neg F(x)$ is proved by lines 7 to 14. The second case is proved in lines 14 to 22. Line 23 is not shown, but would conclude $\exists x. F(x) \rightarrow G(a)$ using 2..5, 6..22 LEM.
Note that one could use LEM on $\exists x. \neg F(x)$ directly to obtain a shorter (but I think conceptually less clear) proof. I'll leave that as an exercise for you.