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. intros L F Hf L' Hl'. apply (filter_notempty F). apply filter_finite_intersection. intros m. apply Hf, Hl'. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.