no goals
α : Type ?u.415768
β : Type u_1
γ : Type ?u.415774
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ ≠ b ↔ b ≠ x✝¹
simp_rw [@ne_comm _ b]