Lemma filtertop_notempty : isfilter_notempty filtertop. Proof. intros A Fa. revert x0. apply hinhfun. intros x0. exists x0. simple refine (Fa _). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.