Lemma common_index {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) (i : I) (x : carrier_subset (⋃ (λ i, S i))) : ∃ j, S i ≼ S j ∧ S j (pr1 x). Proof. induction x as [x xinU]. apply (squash_to_hProp xinU); intros [k xinSk]. change (∃ j : I, S i ≼ S j ∧ S j x). apply (squash_to_hProp (chain i k)). intros c. apply hinhpr. induction c as [c|c]. - exists k. split. + exact c. + exact xinSk. - exists i. split. + apply wosub_le_isrefl. + exact (pr1 c x xinSk). 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.