proposition: Lemma finite_intersections_len_union {X : Type} (F : Family X) : IndexedUnion (finite_intersections_len F) = finite_intersections F.
proof: Proof. apply Extensionality_Ensembles. split. - intros ? [n U HU]. red in HU. dependent induction HU. + apply intro_full. + now apply intro_S. + now apply intro_intersection. - intros ? HU. red in HU. dependent induction HU; try destruct IHHU, IHHU0; econstructor. + constructor. + now apply intro_fi_len_S. + apply intro_fi_len_intersection. * exact H1. * exact H2. Qed.
imports: Coq(ClassicalChoice Lia Program.Equality) ZornsLemma(EnsemblesImplicit InverseImage Proj1SigInjective)