Lemma isdecinclii2 (X Y : UU) : isdecincl (@ii2 X Y). Proof. intros. intro y. induction y as [ x | y ]. - apply (isdecpropif _ (isinclii2 X Y (ii1 x)) (ii2 (neghfiberii2x X Y x))). - apply (isdecpropif _ (isinclii2 X Y (ii2 y)) (ii1 (make_hfiber (@ii2 _ _) y (idpath _)))). Defined.