I'm trying to proof a theorem and currently stuck at :
$$(\exists x |: Q \land \lnot R)\lor(\forall x |: \lnot P \lor R)$$
I believe I can end up with something like :
$$(\forall x|:(Q\land\lnot R)\lor(\lnot P\lor R))$$
From there I'm actually able to complete the proof, but I'm unable to explain how those two are equivalents.
I believe the answer is to use distributivity of $\lor$ over $\exists$:
$$(\exists x |: R) \Rightarrow ( P \lor (\exists x | R:Q) \equiv (\exists x | R : P \lor Q))$$
But I'm then unable to end with the expected result as I get R in the body (which is simply true in my case), but I would instead need P. Is my understanding of distributivity of $\lor$ over $\exists$ incorrect or is it just the wrong theorem to use?
Note: I'm trying to prove a theorem with the form $A\Rightarrow (B \Rightarrow C)$. I started with $B \Rightarrow C$ so I'm expecting to use a $\Leftarrow$ to come back to A.
As far as I can see, I believe the simplest way to cast this proof, is to rewrite your original$$ (\forall x \mid \lnot R : P \Rightarrow Q) \Rightarrow ((\forall x \mid Q : R) \Rightarrow (\forall x \mid P : R)) $$ in the form $\;\ldots \land \ldots \;\Rightarrow\; \ldots\;$, and then simplify the left hand side working towards the right hand side. You should be able to do that without introducing $\;\exists\;$.