Definition stntonat ( n : nat ) : stn n -> nat := @pr1 _ _ .
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.