proposition: Lemma finite_intersections_len_1_in {X : Type} {F : Family X} {U : Ensemble X} : In (finite_intersections_len F 1) U -> In F U.
proof: Proof. intro H. red in H. dependent induction H. - assumption. - destruct m, k; discriminate + injection x as x; subst. + rewrite (finite_intersections_len_0_full_set H), Intersection_Full_set. now apply IHfinite_intersections_len0. + rewrite (finite_intersections_len_0_full_set H0), Intersection_commutative, Intersection_Full_set. apply IHfinite_intersections_len. lia. + lia. Qed.
imports: Coq(Program.Equality) Coq(Lia) Coq(ClassicalChoice) Ensembles EnsemblesImplicit Families FiniteTypes IndexedFamilies CountableTypes Proj1SigInjective Powerset_facts