Lemma negforall_to_existsneg' {X:Type} (P:X->Type) : (¬ ∏ x, ¬¬ (P x)) -> ¬¬ (∃ x, ¬ (P x)). Proof. intros nf c. use nf; clear nf. intro x. assert (q := neghexisttoforallneg _ c x); clear c; simpl in q. exact q. Defined.
Require Import UniMath.Foundations.All.