Definition finite_intersection {X : UU} (P : Sequence (X → hProp)) : X → hProp. Proof. intros x. simple refine (make_hProp _ _). - apply (∏ n, P n x). - apply (impred_isaprop _ (λ _, propproperty _)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.