Lemma filterbase_imply : isfilter_imply filterbase. Proof. intros A B H. apply hinhfun. intros A'. exists (pr1 A'). split. - apply (pr1 (pr2 A')). - intros x Hx. apply H. now apply (pr2 (pr2 A')). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.