proposition: Lemma filterbase_generated_hypothesis : ∏ L' : Sequence (X → hProp), (∏ m : stn (length L'), base (L' m)) → ∃ x : X, finite_intersection L' x.
proof: Proof. intros L Hbase. generalize (base_finite_intersection L Hbase). apply hinhuniv. intros A. generalize (Hfalse _ (pr1 (pr2 A))). apply hinhfun. intros x. exists (pr1 x). apply (pr2 (pr2 A)). exact (pr2 x). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA