Let X and x be given.
Assume Hx: x ∈ X.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ X.
We will prove y ∈ (X ∖ {x}) ∪ {x}.
Apply xm (y ∈ {x}) to the current goal.
Assume H1: y ∈ {x}.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is H1.
Assume H1: y ∉ {x}.
Apply binunionI1 to the current goal.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is H1.
Let y be given.
Assume Hy: y ∈ (X ∖ {x}) ∪ {x}.
Apply binunionE (X ∖ {x}) {x} y Hy to the current goal.
Assume H1: y ∈ X ∖ {x}.
We will prove y ∈ X.
An exact proof term for the current goal is setminusE1 X {x} y H1.
Assume H1: y ∈ {x}.
We will prove y ∈ X.
rewrite the current goal using SingE x y H1 (from left to right).
We will prove x ∈ X.
An exact proof term for the current goal is Hx.
∎