Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ {0} ∪ {(ordsucc m) '|m ∈ 0}.
Apply binunionE {0} {(ordsucc m) '|m ∈ 0} x Hx to the current goal.
Assume Hx: x ∈ {0}.
rewrite the current goal using SingE 0 x Hx (from left to right).
We will prove 0 ∈ 1.
An exact proof term for the current goal is In_0_1.
Assume Hx: x ∈ {(ordsucc m) '|m ∈ 0}.
Apply ReplE_impred 0 (λm ⇒ (ordsucc m) ') x Hx to the current goal.
Let m be given.
Assume Hm: m ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE m Hm.
Let x be given.
Assume Hx: x ∈ 1.
Apply cases_1 x Hx (λx ⇒ x ∈ eps_ 0) to the current goal.
We will prove 0 ∈ {0} ∪ {(ordsucc m) '|m ∈ 0}.
Apply binunionI1 to the current goal.
Apply SingI to the current goal.
∎