Lemma filtergenerated_imply : isfilter_imply filtergenerated. Proof. intros A B H. apply hinhfun ; intro Ha. exists (pr1 Ha), (pr1 (pr2 Ha)). intros x Hx. apply H. apply (pr2 (pr2 Ha)), Hx. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.