fact: Definition chain_union_rel {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) : hrel (carrier_subset (⋃ (λ i, S i))).
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets