Lemma filtergenerated_notempty : isfilter_notempty filtergenerated. Proof. intros A. apply hinhuniv. intros L'. generalize (Hl _ (pr1 (pr2 L'))). apply hinhfun. intros x. exists (pr1 x). apply (pr2 (pr2 L')). exact (pr2 x). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.