proposition: Lemma isdecproplogeqb {X Y : UU} (isx : isaprop X) (isy : isdecprop Y) (lg : X <-> Y) : isdecprop X.
proof: Proof. intros. set (w := weqimplimpl (pr1 lg) (pr2 lg) isx isy). apply (isdecpropweqb w isy). Defined.
imports: UniMath.Foundations.PartA