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