Theorem isdecinclS : isdecincl S. Proof. intro n. apply isdecpropif. - apply (isinclS n). - destruct n as [ | n ]. + assert (nh : ¬ (hfiber S 0)). * intro hf. induction hf as [ m e ]. apply (negpathssx0 _ e). * apply (ii2 nh). + apply (ii1 (make_hfiber _ n (idpath _))). Defined.