Definition decidable_to_DecidableProposition {X : hProp} : decidable X -> DecidableProposition. Proof. intros dec. exists X. now apply decidable_to_isdecprop. Defined.
Require Import UniMath.MoreFoundations.Tactics.