Lemma isincldni ( n : nat ) ( i : ⟦S n⟧ ) : isincl ( dni i ). Proof. intros. exact ( isdecincltoisincl _ ( isdecincldni n i ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.