Lemma filtergenerated_htrue : isfilter_htrue filtergenerated. Proof. apply hinhpr. exists nil. split. + intros m. induction (nopathsfalsetotrue (pr2 m)). + easy. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.