Lemma stn_eq {n : nat} (i i' : stn n) (H : pr1 i = pr1 i') : i = i'. Proof. refine (subtypePath _ H). intro. apply isasetbool. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.