Definition stn_extens {n} (i j : ⟦ n ⟧) (p : stntonat _ i = stntonat _ j) : i = j := subtypePath' p (propproperty (j < n)).
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.