Lemma isdecincldi (i : nat) : isdecincl (di i). Proof. intros j. apply isdecpropif. - apply (isincldi i j). - induction (nat_eq_or_neq i j) as [ eq | neq ]. + apply ii2. induction eq. apply (neghfiberdi i). + apply ii1. apply (pr1 (iscontrhfiberdi i j neq)). Defined.