proposition: Lemma finite_intersections_len_0_full_set {X : Type} {F : Family X} {U : Ensemble X} : In (finite_intersections_len F 0) U -> U = Full_set.
proof: Proof. intro H. red in H. dependent induction H. { reflexivity. } rewrite IHfinite_intersections_len. 2: { lia. } rewrite Intersection_Full_set. rewrite IHfinite_intersections_len0. { reflexivity. } lia. Qed.
imports: Coq(Program.Equality) Coq(Lia) Coq(ClassicalChoice) Ensembles EnsemblesImplicit Families FiniteTypes IndexedFamilies CountableTypes Proj1SigInjective Powerset_facts