proposition: Lemma stn_eq_or_neq {n : nat} (i j: ⟦n⟧ ) : (i=j) ⨿ (i≠j).
proof: Proof. intros. induction (nat_eq_or_neq i j) as [eq|ne]. - apply ii1, subtypePath_prop. assumption. - apply ii2. assumption. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions