Lemma chain_union_rel_istrans {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) : istrans (chain_union_rel chain). Proof. intros x y z l m. apply (squash_to_hProp (common_index3 chain x y z)); intros [i [r [s t]]]. assert (p := chain_union_rel_eqn chain x y i r s). assert (q := chain_union_rel_eqn chain y z i s t). assert (e := chain_union_rel_eqn chain x z i r t). rewrite p in l; clear p. rewrite q in m; clear q. rewrite e; clear e. assert (tot : istrans (WOSrel (S i))). { apply (pr2 (S i)). } exact (tot _ _ _ l m). 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.