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