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