An exact proof term for the current goal is (andEL (well_ordered_set S_Omega) (uncountable_set S_Omega) S_Omega_well_ordered_uncountable).