We will prove Sbar_Omega = ordsucc S_Omega.
Apply set_ext to the current goal.
We will prove Sbar_Omega ⊆ ordsucc S_Omega.
Let y be given.
Assume Hy: y ∈ Sbar_Omega.
We prove the intermediate claim Hy': y ∈ S_Omega ∪ {S_Omega}.
An exact proof term for the current goal is Hy.
Apply (binunionE S_Omega {S_Omega} y Hy') to the current goal.
Assume Hyin: y ∈ S_Omega.
An exact proof term for the current goal is (ordsuccI1 S_Omega y Hyin).
Assume Hyin: y ∈ {S_Omega}.
We prove the intermediate claim Heq: y = S_Omega.
An exact proof term for the current goal is (SingE S_Omega y Hyin).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (ordsuccI2 S_Omega).
We will prove ordsucc S_Omega ⊆ Sbar_Omega.
Let y be given.
Assume Hy: y ∈ ordsucc S_Omega.
Apply (ordsuccE S_Omega y Hy) to the current goal.
Assume Hyin: y ∈ S_Omega.
We prove the intermediate claim Hy': y ∈ S_Omega ∪ {S_Omega}.
An exact proof term for the current goal is (binunionI1 S_Omega {S_Omega} y Hyin).
An exact proof term for the current goal is Hy'.
Assume Heq: y = S_Omega.
We prove the intermediate claim Hy': y ∈ S_Omega ∪ {S_Omega}.
Apply (binunionI2 S_Omega {S_Omega} y) to the current goal.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI S_Omega).
An exact proof term for the current goal is Hy'.
∎