proposition: Lemma chain_union_rel_istotal {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) : istotal (chain_union_rel chain).
proof: Proof. intros x y. apply (squash_to_hProp (common_index2 chain x y)); intros [i [r s]]. assert (p := chain_union_rel_eqn chain x y i r s). rewrite p; clear p. assert (p := chain_union_rel_eqn chain y x i s r). rewrite p; clear p. apply (pr2 (S i)). Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets