Assume HSNo: SNo {1}.
We will prove False.
Set alpha to be the term SNoLev {1}.
We prove the intermediate claim Hlev: ordinal alpha ∧ SNo_ alpha {1}.
An exact proof term for the current goal is (SNoLev_prop {1} HSNo).
We prove the intermediate claim Hord: ordinal alpha.
An exact proof term for the current goal is (andEL (ordinal alpha) (SNo_ alpha {1}) Hlev).
We prove the intermediate claim HSNoa: SNo_ alpha {1}.
An exact proof term for the current goal is (andER (ordinal alpha) (SNo_ alpha {1}) Hlev).
We prove the intermediate claim Hsub: {1} ⊆ SNoElts_ alpha.
An exact proof term for the current goal is (andEL ({1} ⊆ SNoElts_ alpha) (∀beta ∈ alpha, exactly1of2 (beta ' ∈ {1}) (beta ∈ {1})) HSNoa).
We prove the intermediate claim Hprop: ∀beta ∈ alpha, exactly1of2 (beta ' ∈ {1}) (beta ∈ {1}).
An exact proof term for the current goal is (andER ({1} ⊆ SNoElts_ alpha) (∀beta ∈ alpha, exactly1of2 (beta ' ∈ {1}) (beta ∈ {1})) HSNoa).
We prove the intermediate claim H1inElts: 1 ∈ SNoElts_ alpha.
An exact proof term for the current goal is (Hsub 1 (SingI 1)).
We prove the intermediate claim H1inalpha: 1 ∈ alpha.
Apply (binunionE' alpha {beta '|beta ∈ alpha} 1 (1 ∈ alpha)) to the current goal.
Assume H1a: 1 ∈ alpha.
An exact proof term for the current goal is H1a.
Assume H1tag: 1 ∈ {beta '|beta ∈ alpha}.
Apply (ReplE alpha (λbeta : set ⇒ beta ') 1 H1tag) to the current goal.
Let beta be given.
Assume Hbp.
Apply Hbp to the current goal.
Assume Hbetaalpha: beta ∈ alpha.
Assume HtagEq: 1 = beta '.
We will prove 1 ∈ alpha.
Apply FalseE to the current goal.
We prove the intermediate claim Hord1: ordinal 1.
An exact proof term for the current goal is (nat_p_ordinal 1 nat_1).
We prove the intermediate claim HnotOrdTag: ¬ ordinal (beta ').
An exact proof term for the current goal is (tagged_not_ordinal beta).
We prove the intermediate claim HnotOrd1: ¬ ordinal 1.
rewrite the current goal using HtagEq (from left to right) at position 1.
An exact proof term for the current goal is HnotOrdTag.
An exact proof term for the current goal is (HnotOrd1 Hord1).
An exact proof term for the current goal is H1inElts.
We prove the intermediate claim Htr: TransSet alpha.
An exact proof term for the current goal is (ordinal_TransSet alpha Hord).
We prove the intermediate claim H1sub: 1 ⊆ alpha.
An exact proof term for the current goal is (Htr 1 H1inalpha).
We prove the intermediate claim H0inalpha: 0 ∈ alpha.
An exact proof term for the current goal is (H1sub 0 In_0_1).
We prove the intermediate claim Hex01: exactly1of2 (0 ' ∈ {1}) (0 ∈ {1}).
An exact proof term for the current goal is (Hprop 0 H0inalpha).
Apply (exactly1of2_E (0 ' ∈ {1}) (0 ∈ {1}) Hex01 False) to the current goal.
Assume Htag: 0 ' ∈ {1}.
Assume _: ¬ (0 ∈ {1}).
We will prove False.
We prove the intermediate claim HtagEq: 0 ' = 1.
An exact proof term for the current goal is (SingE 1 (0 ') Htag).
We prove the intermediate claim Hord1: ordinal 1.
An exact proof term for the current goal is (nat_p_ordinal 1 nat_1).
We prove the intermediate claim HnotOrdTag: ¬ ordinal (0 ').
An exact proof term for the current goal is (tagged_not_ordinal 0).
We prove the intermediate claim HnotOrd1: ¬ ordinal 1.
rewrite the current goal using HtagEq (from right to left) at position 1.
An exact proof term for the current goal is HnotOrdTag.
An exact proof term for the current goal is (HnotOrd1 Hord1).
Assume _: ¬ (0 ' ∈ {1}).
Assume H0: 0 ∈ {1}.
We will prove False.
We prove the intermediate claim H0eq: 0 = 1.
An exact proof term for the current goal is (SingE 1 0 H0).
An exact proof term for the current goal is (neq_0_1 H0eq).
∎