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