proposition: Lemma chain_union_tosub_le {X : hSet} {I : UU} {S : I → WOSubset X} (Schain : is_wosubset_chain S) (i:I) (inc := subtype_inc (subtype_union_containedIn S i)) : ( S i ≼ ⋃ Schain ) % tosubset.
proof: Proof. exists (subtype_union_containedIn S i). intros s s' j. set (u := subtype_inc (λ x J, hinhpr (i,, J)) s : ⋃ Schain). set (u':= subtype_inc (λ x J, hinhpr (i,, J)) s': ⋃ Schain). change (chain_union_rel Schain u u'). assert (q := chain_union_rel_eqn Schain u u' i (pr2 s) (pr2 s')). rewrite q; clear q. exact j. Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets