no goals
α : Type u_1
β : Type ?u.245796
γ : Type ?u.245799
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ _root_.Disjoint (erase s a) t ↔ _root_.Disjoint s (erase t a)
simp_rw [erase_eq, disjoint_sdiff_comm]