Lemma filterintersection_and : isfilter_and filterintersection. Proof. intros A B Ha Hb F Hf. apply (Hand F Hf). * now simple refine (Ha _ _). * now simple refine (Hb _ _). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.