proposition: Lemma FilterGenerated_inv {X : UU} : ∏ (L : (X → hProp) → hProp) (F : Filter X), (∏ A : X → hProp, L A → F A) → ∏ (L' : Sequence (X → hProp)), (∏ m, L (L' m)) → (∃ x : X, finite_intersection L' x).
proof: Proof. intros L F Hf L' Hl'. apply (filter_notempty F). apply filter_finite_intersection. intros m. apply Hf, Hl'. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA