We will prove ordinal Sbar_Omega.

We prove the intermediate claim Hord: ordinal S_Omega.

An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).

rewrite the current goal using Sbar_Omega_eq_ordsucc (from left to right).

An exact proof term for the current goal is (ordinal_ordsucc S_Omega Hord).

∎