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