Lemma filtertop_and : isfilter_and filtertop. Proof. intros A B Ha Hb x. split. + simple refine (Ha _). + simple refine (Hb _). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.