Lemma negforall_to_existsneg {X:UU} (P:X->hProp) : LEM -> (¬ ∀ x, P x) -> (∃ x, ¬ (P x)). Proof. intros lem nf. apply (proof_by_contradiction lem); intro c. use nf; clear nf. intro x. assert (q := neghexisttoforallneg _ c x); clear c; simpl in q. exact (proof_by_contradiction lem q). Defined.