Lemma isdecprophdisj {X Y : UU} (isx : isdecprop X) (isy : isdecprop Y) : isdecprop (hdisj X Y). Proof. intros. apply isdecpropif. apply (pr2 (hdisj X Y)). induction (pr1 isx) as [ x | nx ]. - apply (ii1 (hinhpr (ii1 x))). - induction (pr1 isy) as [ y | ny ]. + apply (ii1 (hinhpr (ii2 y))). + apply (ii2 (toneghdisj (make_dirprod nx ny))). Defined.