Lemma filterbase_htrue : isfilter_htrue filterbase. Proof. revert Hempty. apply hinhfun. intros A. exists (pr1 A). split. - apply (pr2 A). - intros. exact tt. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.