Lemma filter_forall : ∏ A : X → hProp, (∏ x : X, A x) → F A. Proof. intros A Ha. generalize filter_htrue. apply filter_imply. intros x _. now apply Ha. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.