proposition: Lemma ne : ¬ (i = j).
proof: Proof. apply stnneq_to_nopath. exact tt. Defined.
imports: UniMath.Foundations.Preamble UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.NegativePropositions UniMath.Combinatorics.Lists