proposition: Lemma filter_app3 (T : Type) (F : set_system T) : Filter F -> forall P Q R S : set T, F (fun x => P x -> Q x -> R x -> S x) -> F P -> F Q -> F R -> F S.
proof: Proof. by move=> ????? PQR FP; apply: filter_app2; apply: filter_app FP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed