Corollary dni_lastelement_is_inj {n : nat} {i j : ⟦n⟧ } (e : dni_lastelement i = dni_lastelement j) : i = j. Proof. apply isinjstntonat. unfold dni_lastelement in e. apply (maponpaths pr1) in e. exact e. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.