Definition decidable_to_isdecprop_2 {X : UU} : isaprop X -> X ⨿ ¬ X -> isdecprop X. Proof. intros i dec. apply isdecpropif. - exact i. - exact dec. Defined.
Require Import UniMath.MoreFoundations.Tactics.