Assume Heps2: eps_ 1 ∈ 2.
We will prove False.
We prove the intermediate claim Hsub: 2 ⊆ {0,1}.
An exact proof term for the current goal is Subq_2_UPair01.
We prove the intermediate claim Heps01: eps_ 1 ∈ {0,1}.
An exact proof term for the current goal is (Hsub (eps_ 1) Heps2).
Apply (UPairE (eps_ 1) 0 1 Heps01 False) to the current goal.
Assume Heq0: eps_ 1 = 0.
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Heps1SNoS: eps_ 1 ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega 1 H1omega).
We prove the intermediate claim HepsR: eps_ 1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ 1) Heps1SNoS).
We prove the intermediate claim H0ltEps: Rlt 0 (eps_ 1).
An exact proof term for the current goal is (RltI 0 (eps_ 1) real_0 HepsR (SNo_eps_pos 1 H1omega)).
We prove the intermediate claim Hbad: Rlt 0 0.
rewrite the current goal using Heq0 (from right to left) at position 2.
An exact proof term for the current goal is H0ltEps.
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) Hbad).
Assume Heq1: eps_ 1 = 1.
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Heps1SNoS: eps_ 1 ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega 1 H1omega).
We prove the intermediate claim HepsR: eps_ 1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ 1) Heps1SNoS).
We prove the intermediate claim H0Ord: ordinal 0.
An exact proof term for the current goal is (nat_p_ordinal 0 nat_0).
We prove the intermediate claim H0in1: 0 ∈ 1.
An exact proof term for the current goal is (ordinal_0_In_ordsucc 0 H0Ord).
We prove the intermediate claim HepsLt1S: (eps_ 1) < 1.
We prove the intermediate claim HepsLtE0: eps_ 1 < eps_ 0.
An exact proof term for the current goal is (SNo_eps_decr 1 H1omega 0 H0in1).
rewrite the current goal using (eps_0_1) (from right to left) at position 2.
An exact proof term for the current goal is HepsLtE0.
We prove the intermediate claim HepsLt1: Rlt (eps_ 1) 1.
An exact proof term for the current goal is (RltI (eps_ 1) 1 HepsR real_1 HepsLt1S).
We prove the intermediate claim Hbad: Rlt 1 1.
rewrite the current goal using Heq1 (from right to left) at position 1.
An exact proof term for the current goal is HepsLt1.
An exact proof term for the current goal is ((not_Rlt_refl 1 real_1) Hbad).
∎