Lemma wma_dneg {X:Type} (P:Type) : ¬¬ P -> (P -> ¬ X) -> ¬ X. Proof. intros dnp p. apply dnegnegtoneg. assert (q := dnegf p); clear p. apply q; clear q. apply dnp. Defined.
Require Import UniMath.Foundations.All.