Let k be given.

Assume Hk.

We will prove k ∈ SNoS_ ω.

Apply diadic_rational_p_SNoS_omega to the current goal.

We will prove diadic_rational_p k.

Apply int_diadic_rational_p to the current goal.

An exact proof term for the current goal is Hk.

∎