ext x
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
⊢ ⇑(swap e f) '' S = insert f (S \ {e})
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
⊢ x ∈ ⇑(swap e f) '' S ↔ x ∈ insert f (S \ {e})