Consider the set of inference rules for first order logic (analogous to the ones listed here : http://en.wikipedia.org/wiki/Sequent_calculus#Inference_rules)
I am stuck in proving the following rule
$\vdash_{\gamma} \neg \forall x.\phi \implies \exists x. \neg \phi $
I think it is easy to do this using the notion of soundness and completeness and checking that the left formula is valid when the right is.
However I am not able to prove it using just the formalism of manipulating proof trees with inference rules. Somehow I do not see how to get rid of the negation in $\neg \forall x.\phi$ without applying the rule I want to prove.
Any hints?