Lemma chain_union_rel_isantisymm {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) : isantisymm (chain_union_rel chain). Proof. intros x y l m. change (x=y)%logic. apply (squash_to_hProp (common_index2 chain x y)); intros [i [r s]]. apply subtypePath_prop. assert (p := chain_union_rel_eqn chain x y i r s). rewrite p in l; clear p. assert (q := chain_union_rel_eqn chain y x i s r). rewrite q in m; clear q. assert (anti : isantisymm (WOSrel (S i))). { apply (pr2 (S i)). } assert (b := anti _ _ l m); clear anti l m. exact (maponpaths pr1 b). Defined.
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.