proposition: 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: 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.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets