Lemma FilterTop_correct {X : UU} : ∏ (x0 : ∥ X ∥) (F : Filter X), filter_le F (FilterTop x0). Proof. intros x0 F A Ha. apply PreFilterTop_correct, Ha. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.