Proving this sequent using natural deduction

Question

I'm stuck on proving the following: $$ \forall x(\phi \lor \psi) \vdash \forall x\phi \lor \psi $$ Here, $x$ is not free in $\psi$ but can be free in $\phi$. My proof starts like the following:

1. $\forall x(\phi \lor \psi)$ (premise)
2. $x_0$
3. $\phi[x_0/x] \lor \psi$
4. $\psi$ (assumption)
5. $\forall x\phi \lor \psi$ (or-introduction)
6. $\phi[x_0/x]$ (assumption)
7. ...

And then I'm stuck. In the proof it is like the or-context is in conflict with the $x_0$-context.

Brams28's answer looks correct. But I don't understand why there can't be a simpler proof. The analoguous sequent in propositional logic is just $(p_1 \lor q) \land (p_2 \lor q) \vdash (p_1 \land p_2) \lor q$ which is easily solvable without contradictions.

Answer 1

I don't know exactly what rules you have for the system that you are using, but here is a proof in Fitch, which I'm sure you can convert to your system easily enough. The key is to do a proof by contradiction: