fact: Definition nelstructoncontr {X : UU} (contrx : iscontr X) : nelstruct 1 X := weqcomp weqstn1tounit (invweq (weqcontrtounit contrx)).
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.Subtypes