fact: Definition is_wosubset_chain {X : hSet} {I : UU} (S : I → WOSubset X) := ∀ i j : I, wosub_comparable (S i) (S j).
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets