proposition: Lemma preZFS_isrigid (X : preZFS) : iscontr (X = X).
proof: Proof. apply (pr1contr_to_contr _ (λ x, (ispreZFS x ,, isaprop_ispreZFS x)) X). exact (pr122 X). 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