proposition: Lemma filterdom_and : isfilter_and filterdom.
proof: 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.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA