Definition eqtoweqstn {n n' : nat} (H : n = n') : stn n ≃ stn n'. Proof. use weq_iso. - intro i. refine (make_stn _ i _). abstract exact (transportf (λ x, i < x) H (stnlt i)). - intro i. refine (make_stn _ i _). abstract exact (transportf (λ x, i < x) (!H) (stnlt i)). - abstract (intro i; now apply stn_eq). - abstract (intro i; now apply stn_eq). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.