Needs this proof to be in the library? ``` ¬∃⇒∀¬ : ... {P : Pred A p} → ¬ ∃ (\x → P x) → (∀ x → ¬ P x) ¬∃⇒∀¬ ¬∃P x Px = ¬∃P (x , Px) ``` Also I think that the `reverse' cannot be proved: ``` ¬∀⇒∃¬ : ... ¬ (∀ x → P x) → ∃ (\x → ¬ P x) ``` Can it?
