proposition: Lemma filterdirprod_htrue : isfilter_htrue filterdirprod.
proof: Proof. apply hinhpr. exists (λ _:X, htrue), (λ _:Y, htrue). repeat split. + apply Htrue_x. + apply Htrue_y. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA