Theorem neg_uq_bounded

Proof
01. 1 ⊢ ¬∀x. P x → Q x, hypo.
02. 1 ⊢ ∃x. ¬(P x → Q x), neg_uq 1.
03. 3 ⊢ ¬(P x → Q x), hypo.
04. 3 ⊢ P x ∧ ¬Q x, neg_subj 3.
05. 3 ⊢ ∃x. P x ∧ ¬Q x, ex_intro 4.
06. 1 ⊢ ∃x. P x ∧ ¬Q x, ex_elim 2 5.
neg_uq_bounded. ⊢ (¬∀x. P x → Q x) → (∃x. P x ∧ ¬Q x), subj_intro 6.

Dependencies
The given proof depends on two axioms:
efq, lem.