Definition filternat : (nat → hProp) → hProp := λ P : nat → hProp, ∃ N : nat, ∏ n : nat, N ≤ n → P n.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.