Let n be given.
Assume Hn.
Let m be given.
Assume Hm.
We prove the intermediate claim Lnn: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lmn: nat_p m.
An exact proof term for the current goal is nat_p_trans n Lnn m Hm.
We prove the intermediate claim Lm: m ∈ ω.
An exact proof term for the current goal is nat_p_omega m Lmn.
Apply SNoLtI3 to the current goal.
We will prove SNoLev (eps_ m) ∈ SNoLev (eps_ n).
rewrite the current goal using SNoLev_eps_ m Lm (from left to right).
rewrite the current goal using SNoLev_eps_ n Hn (from left to right).
We will prove ordsucc m ∈ ordsucc n.
An exact proof term for the current goal is nat_ordsucc_in_ordsucc n Lnn m Hm.
We will prove SNoEq_ (SNoLev (eps_ m)) (eps_ n) (eps_ m).
rewrite the current goal using SNoLev_eps_ m Lm (from left to right).
We will prove SNoEq_ (ordsucc m) (eps_ n) (eps_ m).
Let k be given.
Assume Hk: k ∈ ordsucc m.
We will prove k ∈ eps_ n ↔ k ∈ eps_ m.
We prove the intermediate claim Lk: ordinal k.
An exact proof term for the current goal is nat_p_ordinal k (nat_p_trans (ordsucc m) (nat_ordsucc m Lmn) k Hk).
Apply iffI to the current goal.
Assume H1: k ∈ eps_ n.
rewrite the current goal using eps_ordinal_In_eq_0 n k Lk H1 (from left to right).
We will prove 0 ∈ eps_ m.
We will prove 0 ∈ {0} ∪ {(ordsucc j) '|j ∈ m}.
Apply binunionI1 to the current goal.
Apply SingI to the current goal.
Assume H1: k ∈ eps_ m.
rewrite the current goal using eps_ordinal_In_eq_0 m k Lk H1 (from left to right).
We will prove 0 ∈ eps_ n.
We will prove 0 ∈ {0} ∪ {(ordsucc j) '|j ∈ n}.
Apply binunionI1 to the current goal.
Apply SingI to the current goal.
We will prove SNoLev (eps_ m) ∉ eps_ n.
rewrite the current goal using SNoLev_eps_ m Lm (from left to right).
Assume H1: ordsucc m ∈ eps_ n.
Apply neq_ordsucc_0 m to the current goal.
We will prove ordsucc m = 0.
An exact proof term for the current goal is eps_ordinal_In_eq_0 n (ordsucc m) (ordinal_ordsucc m (nat_p_ordinal m Lmn)) H1.
∎