proposition: Corollary isconnectedstn1 : ∏ i1 i2 : ⟦1⟧, i1 = i2.
proof: Proof. intros i1 i2. apply (invmaponpathsweq weqstn1tounit). apply isProofIrrelevantUnit. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions