proposition: Corollary isasetstn ( n : nat ) : isaset (⟦n⟧).
proof: Proof. intro. apply ( isasetifdeceq _ ( isdeceqstn n ) ). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions