proposition: Theorem isaset_preZFS : isaset preZFS.
proof: Proof. simpl. unfold isaset. unfold isaprop. simpl. intros x y p. induction p. intros q. apply (hlevelntosn 0 (x = x) (preZFS_isrigid x) (idpath x) q). Qed.
imports: UniMath.Foundations.PartB UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.HLevels UniMath.Combinatorics.WellOrderedSets UniMath.Combinatorics.OrderedSets UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions