proposition: Theorem preZFS_univalence (X Y : preZFS) : (X = Y) ≃ (preZFS_iso X Y).
proof: Proof. set (P := λ x, λ y, Tree_univalence x y). set (Q := λ x, (ispreZFS x ,, isaprop_ispreZFS x)). exact (substructure_univalence _ _ P Q X Y). 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