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