Definition chain_union_rel_eqn {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) (x y : carrier_subset (⋃ (λ i, S i))) i (s : S i (pr1 x)) (t : S i (pr1 y)) : chain_union_rel chain x y = WOSrel (S i) (pr1 x,,s) (pr1 y,,t). Proof. unfold chain_union_rel. generalize (common_index2 chain x y); intro h. assert (e : hinhpr (i,,s,,t) = h). { apply propproperty. } now induction e. 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.