Definition decrel_to_DecidableRelation {X : UU} : decrel X -> DecidableRelation X. Proof. intros R x y. induction R as [R is]. exists (R x y). apply isdecpropif. { apply propproperty. } apply is. Defined.
Require Import UniMath.MoreFoundations.Tactics.