Lemma dneg_decidable (P:Type) : ¬¬ decidable P. Proof. intros ndec. unfold decidable in ndec. assert (q := fromnegcoprod ndec); clear ndec. contradicts (pr1 q) (pr2 q). Defined.
Require Import UniMath.Foundations.All.