Definition decidable_to_isdecprop {X : hProp} : decidable X -> isdecprop X. Proof. intros dec. apply isdecpropif. - apply propproperty. - exact dec. Defined.
Require Import UniMath.MoreFoundations.Tactics.