proposition: Corollary iscontrstn1 : iscontr (⟦1⟧).
proof: Proof. apply iscontrifweqtounit. apply weqstn1tounit. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions