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