proposition: Lemma filter_fromT_filter {I T : Type} (B : I -> set T) : (exists _ : I, True) -> (forall i j, exists k, B k `<=` B i `&` B j) -> Filter (filter_from setT B).
proof: Proof. move=> [i0 _] BI; apply: filter_from_filter; first by exists i0. by move=> i j _ _; have [k] := BI i j; exists k. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed