Need Help With First Order Intuitionistic Tableaux

Question

I have a question about semantic tableaux for Intuitionistic FOL. I’ll post a sample tableaux that I’m pretty sure I’m doing wrong, and then I’ll post a sequent calculus approach to show where I get stuck.

Here’s the tableaux:

1. $\forall x (Fx \lor Gx),0+$

2. $\forall x Fx \lor \exists x Gx,0-$

3. $\forall x Fx,0-$ (line 2)

4. $\exists x Gx,0-$ (line 2; line 2 discharged)

   $0R1$

5. $Fa,1-$ (line 3; line 3 discharged)

6. $Ga,0-$ (line 4)

7. $Fa \lor Ga,0+$ (line 1)

   8. $Fa,0+$ (line 7)

   9. $Fa,1+$ (line 8)

      $\bot$

   10. $Ga, 0+$ (line 7)

       $\bot$

   $\bot$

Here’s the sequent calculus:

$\dfrac{Fx,\forall x (Fx \lor Gx) \vdash \exists x Gx |Gx, \forall x (Fx \lor Gx) \vdash Gx}{\dfrac{Fx,\forall x (Fx \lor Gx) \vdash \exists x Gx |Gx, \forall x (Fx \lor Gx) \vdash \exists x Gx}{\dfrac{Fx \lor Gx, \forall x (Fx \lor Gx) \vdash \exists x Gx}{\dfrac{Fx \lor Gx, \forall x (Fx \lor Gx) \vdash \forall x Fx \lor \exists x Gx}{\dfrac{\forall x (Fx \lor Gx),\forall x (Fx \lor Gx) \vdash \forall x Fx \lor \exists x Gx}{\dfrac{\forall x (Fx \lor Gx)\vdash \forall x Fx \lor \exists x Gx}{\vdash \forall x (Fx \lor Gx) \to (\forall x Fx \lor \exists x Gx)}}}}}}$

Unless I’m not seeing something obvious, I don’t know how to prove this with sequent calculus. Any help would be appreciated.