∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → β} (p : Set β → Prop) {s : Set β}
  [h' : HasCountableSeparatingOn β p s],
  (∀ᶠ (x : α) in l, f x ∈ s) →
    (∀ᶠ (x : α) in l, g x ∈ s) → (∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U) → f =ᶠ[l] g