Lemma chain_union_prelim_eq0 {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) (x y : X) (i j: I) (xi : S i x) (xj : S j x) (yi : S i y) (yj : S j y) : WOSrel (S i) (x ,, xi) (y ,, yi) = WOSrel (S j) (x ,, xj) (y ,, yj). Proof. apply weqlogeq. apply (squash_to_hProp (chain i j)). intros [c|c]. - split. + intro l. assert (q := wosub_le_comp c _ _ l); clear l. now apply (h1'' q). + intro l. apply (pr2 ((wosub_fidelity c) (x,,xi) (y,,yi))). now apply (@h1'' X (S j) _ _ _ _ l). - split. + intro l. apply (pr2 ((wosub_fidelity c) (x,,xj) (y,,yj))). now apply (@h1'' X (S i) _ _ _ _ l). + intro l. assert (q := wosub_le_comp c _ _ l); clear l. now apply (h1'' q). 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.