Lemma PreFilterTop_correct {X : UU} : ∏ (F : PreFilter X), filter_le F PreFilterTop. Proof. intros F A Ha. apply filter_forall, Ha. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.