Lemma filternat_imply : isfilter_imply filternat. Proof. intros P Q H. apply hinhfun. intros N. exists (pr1 N). intros n Hn. now apply H, (pr2 N). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.