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