Lemma filterdom_and : isfilter_and filterdom. Proof. intros A B Ha Hb. generalize (Hand _ _ Ha Hb). apply Himp. intros x ABx Hx. split. - apply (pr1 ABx), Hx. - apply (pr2 ABx), Hx. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.