proposition: Lemma filtergenerated_notempty : isfilter_notempty filtergenerated.
proof: 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.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA