Lemma filterintersection_notempty : isfilter_notempty filterintersection. Proof. intros A Fa. revert His. apply hinhuniv. intros F. apply (Hempty (pr1 F)). * exact (pr2 F). * simple refine (Fa _ _). exact (pr2 F). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.