no goals
α : Type u_1
β : Type ?u.321046
γ : Type ?u.321049
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
a : α
⊢ a ∈ filter (fun x => False) s ↔ a ∈ ∅
simp [mem_filter, and_false_iff]