Let X be given.
Apply set_ext to the current goal.
Let x be given.
Assume H1: x ∈ Empty ∪ X.
Apply (binunionE Empty X x H1) to the current goal.
Assume H2: x ∈ Empty.
We will prove False.
An exact proof term for the current goal is (EmptyE x H2).
Assume H2: x ∈ X.
An exact proof term for the current goal is H2.
Let x be given.
Assume H2: x ∈ X.
We will prove x ∈ Empty ∪ X.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is H2.
∎