proposition: Lemma isdecincldi (i : nat) : isdecincl (di i).
proof: 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.
imports: UniMath.Foundations.Sets