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