Lemma neg_isdecprop {X : UU} : isdecprop X -> isdecprop (¬ X). Proof. intros i. set (j := isdecproptoisaprop X i). apply isdecpropif. - apply isapropneg. - unfold isdecprop in i. set (k := pr1 i). induction k as [k|k]. + apply ii2. now apply todneg. + now apply ii1. Defined.
Require Import UniMath.MoreFoundations.Tactics.