Lemma chain_union_rel_isrefl {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) : isrefl (chain_union_rel chain). Proof. intros x. apply (squash_to_hProp (pr2 x)). intros [i r]. assert (p := chain_union_rel_eqn chain x x i r r). rewrite p; clear p. apply (pr2 (S i)). 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.