Definition isfilter_finite_intersection := ∏ (L : Sequence (X → hProp)), (∏ n, F (L n)) → F (finite_intersection L).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.