proposition: Lemma near_acc T F (P : @in_filter T F) (Q : set T) (FF : Filter F) (FQ : \forall x \near F, Q x) : locked_with near_key (forall x, prop_of (in_filterI FF P (InFilter FQ)) x -> Q x).
proof: Proof. by rewrite unlock => x /=; rewrite !prop_ofE /= => -[Px]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed