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