Definition isfilter_imply := ∏ A B : X → hProp, (∏ x : X, A x → B x) → F A → F B.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.