proposition: Lemma negforall_to_existsneg {X:UU} (P:X->hProp) : LEM -> (¬ ∀ x, P x) -> (∃ x, ¬ (P x)).
proof: 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.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions