Lemma dni_neq_i {n : nat} (i : ⟦S n⟧) (j : ⟦n⟧ ) : i ≠ @dni n i j. Proof. intros. simpl. apply di_neq_i. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.