Let n be given.
Assume Hn.
We prove the intermediate claim Ln: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We will prove eps_ n ⊆ SNoElts_ (ordsucc n) ∧ ∀m ∈ ordsucc n, exactly1of2 (m ' ∈ eps_ n) (m ∈ eps_ n).
Apply andI to the current goal.
Let x be given.
Assume Hx: x ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.
Apply binunionE {0} {(ordsucc m) '|m ∈ n} 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 ∈ SNoElts_ (ordsucc n).
We will prove 0 ∈ ordsucc n ∪ {β '|β ∈ ordsucc n}.
Apply binunionI1 to the current goal.
We will prove 0 ∈ ordsucc n.
An exact proof term for the current goal is nat_0_in_ordsucc n Ln.
Assume Hx: x ∈ {(ordsucc m) '|m ∈ n}.
Apply ReplE_impred n (λm ⇒ (ordsucc m) ') x Hx to the current goal.
Let m be given.
Assume Hm: m ∈ n.
Assume Hxm: x = (ordsucc m) '.
We will prove x ∈ SNoElts_ (ordsucc n).
We will prove x ∈ ordsucc n ∪ {β '|β ∈ ordsucc n}.
Apply binunionI2 to the current goal.
We will prove x ∈ {β '|β ∈ ordsucc n}.
rewrite the current goal using Hxm (from left to right).
We will prove (ordsucc m) ' ∈ {β '|β ∈ ordsucc n}.
An exact proof term for the current goal is ReplI (ordsucc n) (λβ ⇒ β ') (ordsucc m) (nat_ordsucc_in_ordsucc n Ln m Hm).
Let m be given.
Assume Hm: m ∈ ordsucc n.
We prove the intermediate claim Lm: nat_p m.
An exact proof term for the current goal is nat_p_trans (ordsucc n) (nat_ordsucc n Ln) m Hm.
Apply nat_inv m Lm to the current goal.
Assume Hm: m = 0.
rewrite the current goal using Hm (from left to right).
Apply exactly1of2_I2 to the current goal.
We will prove 0 ' ∉ eps_ n.
Assume H1: 0 ' ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.
Apply binunionE {0} {(ordsucc m) '|m ∈ n} (0 ') H1 to the current goal.
Assume H2: 0 ' ∈ {0}.
Apply EmptyE {1} to the current goal.
We will prove {1} ∈ 0.
rewrite the current goal using SingE 0 (0 ') H2 (from right to left) at position 2.
We will prove {1} ∈ 0 '.
We will prove {1} ∈ 0 ∪ {{1}}.
Apply binunionI2 to the current goal.
We will prove {1} ∈ {{1}}.
Apply SingI to the current goal.
Assume H2: 0 ' ∈ {(ordsucc m) '|m ∈ n}.
Apply ReplE_impred n (λm ⇒ (ordsucc m) ') (0 ') H2 to the current goal.
Let m be given.
Assume Hm: m ∈ n.
Assume H3: 0 ' = (ordsucc m) '.
Apply neq_0_ordsucc m to the current goal.
We will prove 0 = ordsucc m.
Apply tagged_eqE_eq to the current goal.
We will prove ordinal 0.
An exact proof term for the current goal is ordinal_Empty.
We will prove ordinal (ordsucc m).
An exact proof term for the current goal is (nat_p_ordinal (ordsucc m) (nat_ordsucc m (nat_p_trans n Ln m Hm))).
We will prove 0 ' = (ordsucc m) '.
An exact proof term for the current goal is H3.
We will prove 0 ∈ eps_ n.
We will prove 0 ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is SingI 0.
Assume H1.
Apply H1 to the current goal.
Let k be given.
Assume H1.
Apply H1 to the current goal.
Assume Hk: nat_p k.
Assume Hmk: m = ordsucc k.
We prove the intermediate claim Lm: nat_p m.
rewrite the current goal using Hmk (from left to right).
An exact proof term for the current goal is nat_ordsucc k Hk.
We prove the intermediate claim LSk: ordsucc k ∈ ordsucc n.
rewrite the current goal using Hmk (from right to left).
An exact proof term for the current goal is Hm.
We prove the intermediate claim Lk: k ∈ n.
Apply ordsuccE n (ordsucc k) LSk to the current goal.
Assume H2: ordsucc k ∈ n.
Apply nat_trans n Ln (ordsucc k) H2 to the current goal.
We will prove k ∈ ordsucc k.
Apply ordsuccI2 to the current goal.
Assume H2: ordsucc k = n.
rewrite the current goal using H2 (from right to left).
Apply ordsuccI2 to the current goal.
Apply exactly1of2_I1 to the current goal.
We will prove m ' ∈ eps_ n.
We will prove m ' ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.
Apply binunionI2 to the current goal.
rewrite the current goal using Hmk (from left to right).
We will prove (ordsucc k) ' ∈ {(ordsucc m) '|m ∈ n}.
An exact proof term for the current goal is ReplI n (λk ⇒ (ordsucc k) ') k Lk.
We will prove m ∉ eps_ n.
Assume H1: m ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.
Apply binunionE {0} {(ordsucc m) '|m ∈ n} m H1 to the current goal.
Assume H2: m ∈ {0}.
Apply EmptyE 0 to the current goal.
We will prove 0 ∈ 0.
rewrite the current goal using SingE 0 m H2 (from right to left) at position 2.
We will prove 0 ∈ m.
rewrite the current goal using Hmk (from left to right).
An exact proof term for the current goal is nat_0_in_ordsucc k Hk.
Assume H2: m ∈ {(ordsucc j) '|j ∈ n}.
Apply ReplE_impred n (λj ⇒ (ordsucc j) ') m H2 to the current goal.
Let j be given.
Assume Hj: j ∈ n.
Assume Hmj: m = (ordsucc j) '.
Apply tagged_not_ordinal (ordsucc j) to the current goal.
We will prove ordinal ((ordsucc j) ').
rewrite the current goal using Hmj (from right to left).
We will prove ordinal m.
An exact proof term for the current goal is nat_p_ordinal m Lm.
∎