proposition: Lemma filterdom_imply : isfilter_imply filterdom.
proof: Proof. intros A B Himpl. apply Himp. intros x Ax Hx. apply Himpl, Ax, Hx. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA