fact: Definition isfilter_finite_intersection := ∏ (L : Sequence (X → hProp)), (∏ n, F (L n)) → F (finite_intersection L).
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA