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