Definition decidableNot (P : DecidableProposition) : DecidableProposition. Proof. intros. exists (¬ P). apply neg_isdecprop; apply decidabilityProperty. Defined.
Require Import UniMath.MoreFoundations.Tactics.