proposition: Lemma isinjstntonat (n : nat) : isInjectiveFunction (pr1 : stnset n -> natset).
proof: Proof. intros i j. apply subtypePath_prop. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions